X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;fp=src%2FHaskCoreToWeak.v;h=b538417f84e5c0b0f67422c941ef4fa046b884a0;hp=644d04d8e70f629c235f28f053c0abcd2dc2b8f1;hb=1f411b48dd607e76a65903e8506d0ae5e7470321;hpb=1758dade15ff584949a9e4bd6b21ce1a58e42ff3

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 644d04d..b538417 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -102,7 +102,7 @@ Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
   let (t1,t2) := coreCoercionKind cc
   in  coreTypeToWeakType t1 >>= fun t1' =>
     coreTypeToWeakType t2 >>= fun t2' =>
-    OK (weakCoercion t1' t2' cc).
+    OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with