X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;fp=src%2FHaskWeak.v;h=9d39f44c14e63f69ecc541e34f06df3eeb5c4144;hp=077f7b509a22032859a83729226a7fc82b2620fe;hb=025c2de2effdd7177ca875998b65f51236c8c7c6;hpb=be7ab3c195d3d5c4e7883b090c68fa56df2b1dcb

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 077f7b5..9d39f44 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -31,6 +31,10 @@ Inductive WeakExpr :=
 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+(*
+| WEKappa     : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+| WEKappaApp  : WeakExpr                        -> WeakExpr                  -> WeakExpr
+*)
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr