X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskStrong.v;h=611a4c8aec813069ef2b3653d59141aca1f92650;hb=30cc675d57492799644506f3632625f371a3e89a;hp=8efd0af15b870e57baf712d8d4d3906cc341ca49;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda;p=coq-hetmet.git

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 8efd0af..611a4c8 100644
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -31,6 +31,10 @@ Section HaskStrong.
   Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.
 
   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
+
+  (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
+  | EGlobal: ∀ Γ Δ ξ t,       WeakExprVar ->                                                         Expr Γ Δ ξ t
+
   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
   | EApp   : ∀ Γ Δ ξ t1 t2 l,        Expr Γ Δ ξ (t2--->t1 @@ l)   -> Expr Γ Δ ξ (t2 @@ l)         -> Expr Γ Δ ξ (t1 @@ l)