X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=013c62a6b7044f8b2dbfcc1858ed709182cbc073;hp=e5a2bfb8b2fc11da5f2fd2c39fa0afd7b94ad3ad;hb=ee5aaad57d76400e9b8736d4a12d2804f99f329c;hpb=26733c04106397dc8a10396ce688e908e8d0cde7

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index e5a2bfb..013c62a 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -35,8 +35,8 @@ Inductive WeakExpr :=
 | WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 | WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 
-(* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
-| WECase      : forall (scrutinee:WeakExpr)
+| WECase      : forall (vscrut:WeakExprVar)
+                       (scrutinee:WeakExpr)
                        (tbranches:WeakType)
                        (tc:TyCon)
                        (type_params:list WeakType)
@@ -125,7 +125,7 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
     | WELetRec rb e              => weakTypeOfWeakExpr e
     | WENote  n e                => weakTypeOfWeakExpr e
     | WECast  e (weakCoercion _ t1 t2 _) => OK t2
-    | WECase  scrutinee tbranches tc type_params alts => OK tbranches
+    | WECase  vscrut scrutinee tbranches tc type_params alts => OK tbranches
 
     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
     | WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')