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

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 2c418bd..611a4c8 100644
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -8,10 +8,10 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskWeakVars.
 Require Import HaskCoreTypes.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
+Require Import HaskWeakVars.
 
 Section HaskStrong.
 
@@ -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)