Minor improvement

1 year ago · 9f77d69dcf
parent 1f956e528e
commit 9f77d69dcf
1 changed files with 2 additions and 4 deletions
--- a/theories/type_systems/stlc_extended/bigstep.v
+++ b/theories/type_systems/stlc_extended/bigstep.v
@ -1,14 +1,12 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.ts.stlc_extended Require Import lang notation types.
+From semantics.ts.stlc_extended Require Import lang notation.

 (** * Big-step semantics *)

 Implicit Types
-  (Γ : typing_context)
  (v : val)
-  (e : expr)
-  (A : type).
+  (e : expr).

 Inductive big_step : expr → val → Prop :=
  | bs_lit (n : Z) :