X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=51e61dd83aadac32525973479c7ad91b385362d9;hb=30cc675d57492799644506f3632625f371a3e89a;hp=c97a63cef20a810160a3b07d51e277358f434939;hpb=14a87dd821c4194382f29eef2d59fe932d4124c1;p=coq-hetmet.git

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index c97a63c..51e61dd 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -95,8 +95,8 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                                      nil)
                                                    (CoreEVar v)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
-  | WECase  vscrut e tbranches tc types alts  =>
-                                            CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
+  | WECase  vscrut escrut tbranches tc types alts  =>
+                                            CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 
                                                   ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=