X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=dacdcae45f240a7aef6e0d3c30d4aa04f8cad629;hp=cbe67152bca59a768cb45cd5aca9ddb053a12bdc;hb=539d675a181f178e24c15b2a6ad3c990492eed79;hpb=8f00501ac48984925832279f7d67302c09a570ec

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index cbe6715..dacdcae 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -194,7 +194,7 @@ Section HaskStrongToWeak.
     match elrb as E in ELetRecBindings G D X L V
        return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
     | ELR_nil    _ _ _ _           => fun ite => return []
-    | ELR_leaf   _ _ ξ' cv v e     => fun ite => bind t'  = typeToWeakType (unlev (ξ' v)) ite
+    | ELR_leaf   _ _ ξ' cv v t e   => fun ite => bind t'  = typeToWeakType t ite
                                                ; bind e'  = exprToWeakExpr χ e ite
                                                ; bind v'  = match χ v with Error s => failM s | OK y => return y end
                                                ; return [(v',e')]