Debugging code commented out.

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index eeff1fa968f2e382e60646aae79397f4cc5f5551..1de14927049ad475414aa95d05f2b55ab184b9c2 100644 (file)
--- 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)
 ;;