X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCore.v;h=13a263ed89ef83f0fd4d75aac97b4229de569377;hp=b05c34f2937bd679e3f36265d1badf398018a2cc;hb=0f137f4fbe7076b7a0f6b33d661b4f7aa8b4f160;hpb=d97b00a6ff6e8e2244927d17bda4b9762fc3d716

diff --git a/src/HaskCore.v b/src/HaskCore.v
index b05c34f..13a263e 100644
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -23,6 +23,7 @@ Inductive CoreExpr {b:Type} :=
 | CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
 | CoreENote  : Note            ->  CoreExpr     -> CoreExpr
 | CoreEType  : CoreType                         -> CoreExpr
+| CoreECoercion : CoreCoercion                  -> CoreExpr
 with      CoreBind {b:Type} :=
 | CoreNonRec : b -> CoreExpr         -> CoreBind  
 | CoreRec    : list (b * CoreExpr  ) -> CoreBind.
@@ -36,7 +37,9 @@ Extract Inductive CoreExpr =>
       "CoreSyn.Case"
       "CoreSyn.Cast"
       "CoreSyn.Note"
-      "CoreSyn.Type" ].
+      "CoreSyn.Type"
+      "CoreSyn.Coercion"
+   ].
 Extract Inductive CoreBind =>
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].