X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;fp=src%2FHaskCoreToWeak.v;h=055d588c4be89aff7959012fbc7556c55220685c;hp=c4bd768d69ca1e4b373242bce7ceb4f5b112d0d3;hb=693c6f552555f14c085a71e0b03c67d3c051eaa1;hpb=14a87dd821c4194382f29eef2d59fe932d4124c1

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index c4bd768..055d588 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -218,9 +218,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 
         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
-        coreExprToWeakExpr e >>= fun e' =>
           expectTyConApp te' nil >>= fun tca =>
-            let (tc,lt) := tca in
+            let (tc,lt) := tca:(TyCon * list WeakType) in
           ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
             match branches with