From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Dec 2006 18:48:00 +0000 (+0000)
Subject: Debugging code commented out.
X-Git-Tag: make_still_working~6589
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=842e504b575199aab7bca96c01b3c5d8ef28f712;p=helm.git

Debugging code commented out.
---

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index eeff1fa96..1de149270 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -93,7 +93,7 @@ let index univ key term =
   (* flexible terms are not indexed *)
   if key = Cic.Meta(-1,[]) then univ
   else
-    (prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
+    ((*prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);*)
      TI.index univ key term)
 ;;