X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrong.v;h=d52acb959fc168ee3d43b01a3d70d51109d0e252;hp=478985da81f4d9629c8affceb7682cf0a15c3849;hb=013a93a8fbae4b8c8df290e9eff226f786770762;hpb=1cfe65d4e2d3292cc038882d8518dd7a48e2c40a

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 478985d..d52acb9 100644
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -9,7 +9,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskWeakVars.
 Require Import HaskCoreVars.
@@ -31,7 +32,7 @@ Section HaskStrong.
   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
+  | EGlobal: forall Γ Δ ξ   (g:Global Γ) v lev,                                                      Expr Γ Δ ξ (g v @@ lev)
 
   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
@@ -79,7 +80,7 @@ Section HaskStrong.
   Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
     match exp with
     | EVar  Γ' _ ξ' ev              => "var."+++ toString ev
-    | EGlobal Γ' _ ξ' t wev         => "global." +++ toString (wev:CoreVar)
+    | EGlobal Γ' _ ξ'   g v _       => "global." +++ toString (g:CoreVar)
     | ELam  Γ'   _ _ tv _ _ cv e    => "\("+++ toString cv +++":t) -> "+++ exprToString e
     | ELet  Γ' _ _ t _ _ ev e1 e2   => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
     | ELit  _ _ _ lit _             => "lit."+++toString lit