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

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