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: 0.4.95@7852~730
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5aa1f1918c39c0d4130574927fa0f870e613cdea;p=helm.git

Debugging code commented out.
---

diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml
index eeff1fa96..1de149270 100644
--- a/components/tactics/universe.ml
+++ b/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)
 ;;