X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;fp=src%2FHaskWeakToStrong.v;h=f6dc70149d77fff47d45a0adeffdd113f446caa0;hp=0acc0af06f750046066236e227305f253a00d48b;hb=025c2de2effdd7177ca875998b65f51236c8c7c6;hpb=be7ab3c195d3d5c4e7883b090c68fa56df2b1dcb

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 0acc0af..f6dc701 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -489,6 +489,10 @@ Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
     | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
     | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
     | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+(*
+    | WEKappaApp  e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+    | WEKappa  cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+*)
     | WETyLam  cv e     => doesWeakVarOccur wev e
     | WECoLam  cv e     => doesWeakVarOccur wev e
     | WECase vscrut escrut tbranches tc avars alts =>