]> matita.cs.unibo.it Git - helm.git/commitdiff
Debugging code commented out.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Dec 2006 18:48:00 +0000 (18:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Dec 2006 18:48:00 +0000 (18:48 +0000)
helm/software/components/tactics/universe.ml

index eeff1fa968f2e382e60646aae79397f4cc5f5551..1de14927049ad475414aa95d05f2b55ab184b9c2 100644 (file)
@@ -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)
 ;;