X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=c3e90a43763c820af3ea4c561b465986d05a73ad;hp=8ceb0b73265c947b1505dfdc1fd50f4263986ee6;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=14afe39e905be69eabd8944b97bb2b731bf44939

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 8ceb0b7..c3e90a4 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -25,13 +25,6 @@ Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@trip
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
-Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
-    Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
-
-(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
-Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
-  Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
-
 Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
   match wa with
   | WeakDataAlt cdc => DataAlt cdc
@@ -59,7 +52,7 @@ Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
   end.
 
 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
-  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
+  CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
@@ -67,8 +60,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   | WELit   lit                          => CoreELit  lit
   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
-  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
-                                                           (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
+  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co))
   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )