X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=9d39f44c14e63f69ecc541e34f06df3eeb5c4144;hp=670d8bda940ea112749d3e23ea339c57e7038cbd;hb=dadeee86855fd6acf1ba00778fe12c1e425f1842;hpb=e0435a27dee3f76fb6f8daf493f583cbd1b4cc72

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 670d8bd..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
 
@@ -108,4 +112,4 @@ Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr :=
   (* un-letrec-ify multi branch letrecs *)
   | WELetRec mlr e                       => WELetRec mlr (simplifyWeakExpr e )
   end.
-*)
\ No newline at end of file
+*)