X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;fp=src%2FHaskCoreToWeak.v;h=a812483bc7ded9f0e91dddeb8c1188e55628ac23;hp=6fc5b431ea1cdee2c9e15b70bf05d5ba4cad4fa6;hb=ee5aaad57d76400e9b8736d4a12d2804f99f329c;hpb=26733c04106397dc8a10396ce688e908e8d0cde7

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 6fc5b43..a812483 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -200,7 +200,10 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
           >>= fun branches =>
             coreExprToWeakExpr e >>= fun scrutinee =>
               coreTypeToWeakType tbranches >>= fun tbranches' =>
-                  OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))
+                  OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
       end
   end.
 
+
+
+