Merge branch 'master' of http://git.megacz.com/coq-hetmet

[coq-hetmet.git] / src / HaskWeak.v

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 670d8bd..9d39f44 100644 (file)
--- 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
+*)