update for new GHC coercion representation

[coq-hetmet.git] / src / HaskCore.v

diff --git a/src/HaskCore.v b/src/HaskCore.v
index 9024828..13a263e 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 

@@ -22,6 +23,7 @@ Inductive CoreExpr {b:Type} :=
 | CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
 | CoreENote  : Note            ->  CoreExpr     -> CoreExpr
 | CoreEType  : CoreType                         -> CoreExpr
 | 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.
 with      CoreBind {b:Type} :=
 | CoreNonRec : b -> CoreExpr         -> CoreBind  
 | CoreRec    : list (b * CoreExpr  ) -> CoreBind.

@@ -35,7 +37,9 @@ Extract Inductive CoreExpr =>
       "CoreSyn.Case"
       "CoreSyn.Cast"
       "CoreSyn.Note"
       "CoreSyn.Case"
       "CoreSyn.Cast"
       "CoreSyn.Note"

-      "CoreSyn.Type" ].
+      "CoreSyn.Type"
+      "CoreSyn.Coercion"
+   ].

 Extract Inductive CoreBind =>
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
 
 Extract Inductive CoreBind =>
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].