X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;fp=src%2FHaskWeakToCore.v;h=39871a3ef33f93ccb4e968ce4c681482807c0f05;hp=c97a63cef20a810160a3b07d51e277358f434939;hb=c9a110c17f24f89f0375c3207b7c544e87a3cee8;hpb=6b017fc7346850c589273befe5faef9ee57bd53d

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index c97a63c..39871a3 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -60,8 +60,10 @@ Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
                                             (weakTypeToCoreType t3)
   end.
 
-Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
-  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion.
+  admit.
+  Defined.
+  (*mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).*)
 
 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with