X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakToCore.v;fp=src%2FHaskWeakToCore.v;h=51e61dd83aadac32525973479c7ad91b385362d9;hb=601b57023dd6fe4295c5af8bb3f5c508618a5f64;hp=c97a63cef20a810160a3b07d51e277358f434939;hpb=553474663acbc6a2ee360497e9d943d3c0b3ccb5;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)) :=