X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;fp=src%2FHaskWeak.v;h=78cd6aedb8f6c8fef9ef3aa50fb32b5aa4e174cc;hp=537bfbe0512a4817d6b489b0c23e6e654255035d;hb=5c493a75fbaf8454d8a21e55edc5b193e2c5879c;hpb=6232ffa2805211654c6ff40a9852d7fc312382d2

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 537bfbe..78cd6ae 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -43,6 +43,7 @@ Inductive WeakExpr :=
                        WeakExpr.
 
 (* calculate the free WeakVar's in a WeakExpr *)
+(*
 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
   match me with
     | WELit    _        =>     nil
@@ -92,7 +93,7 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr :=
     | nil      => me
     | cv::cvl' => WELam cv (closeExpression me cvl')
   end) me (getWeakExprFreeVars me).
-
+*)
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).