X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCore.v;h=64699fd4a4a1f757dfa41b38ce07b1fff0104456;hp=e9f39298710b5bdc26d6dd2ee9735aae4639f01f;hb=703bff3b209bd7d114b49cb736da8af167a4ec71;hpb=5a0761840d89b82cdacb0bf9215fd41aba847b68

diff --git a/src/HaskCore.v b/src/HaskCore.v
index e9f3929..64699fd 100644
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -12,19 +12,19 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
 (* this type must extract to EXACTLY match TypeRep.Type *)
-Inductive CoreExpr (b:Type) :=
-| CoreEVar   : CoreVar                          -> CoreExpr b
-| CoreELit   : HaskLiteral                      -> CoreExpr b
-| CoreEApp   : CoreExpr b      ->  CoreExpr b   -> CoreExpr b
-| CoreELam   :          b      ->  CoreExpr b   -> CoreExpr b
-| CoreELet   : CoreBind b      ->  CoreExpr b   -> CoreExpr b
-| CoreECase  : CoreExpr b -> b ->  CoreType     -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b
-| CoreECast  : CoreExpr b      ->  CoreCoercion -> CoreExpr b
-| CoreENote  : Note            ->  CoreExpr b   -> CoreExpr b
-| CoreEType  : CoreType                         -> CoreExpr b
-with      CoreBind (b:Type) :=
-| CoreNonRec : b -> CoreExpr b       -> CoreBind b
-| CoreRec    : list (b * CoreExpr b) -> CoreBind b.
+Inductive CoreExpr {b:Type} :=
+| CoreEVar   : CoreVar                          -> CoreExpr
+| CoreELit   : HaskLiteral                      -> CoreExpr
+| CoreEApp   : CoreExpr        ->  CoreExpr     -> CoreExpr
+| CoreELam   : b               ->  CoreExpr     -> CoreExpr
+| CoreELet   : CoreBind        ->  CoreExpr     -> CoreExpr
+| CoreECase  : CoreExpr   -> b ->  CoreType     -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr
+| CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
+| CoreENote  : Note            ->  CoreExpr     -> CoreExpr
+| CoreEType  : CoreType                         -> CoreExpr
+with      CoreBind {b:Type} :=
+| CoreNonRec : b -> CoreExpr         -> CoreBind  
+| CoreRec    : list (b * CoreExpr  ) -> CoreBind.
 Extract Inductive CoreExpr =>
    "CoreSyn.Expr" [
       "CoreSyn.Var"