restore HaskWeakToStrong functionality that I broke over the weekend

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

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 644d04d..b538417 100644 (file)
--- 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' =>
   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
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with