Disabled debug prints in the inversion principle.

diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml
index 13b350daf07f996a8142b177c3384bb59510c856..fa4b71178a7886ba20c3ded480c323c0e4ea3b50 100644 (file)
--- a/helm/software/components/tactics/inversion.ml
+++ b/helm/software/components/tactics/inversion.ml
@@ -28,7 +28,7 @@
 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
 exception NotAnInductiveTypeToEliminate
 
-let debug = true;; 
+let debug = false;; 
 let debug_print =
  fun msg -> if debug then prerr_endline (Lazy.force msg) else ()
 

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index e15e8cb630a0eed2ab9543a34eab41f178d61c4e..3229a261b46f82640d05a52a78ece4ecc4dabd3b 100644 (file)
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let debug = true;; 
+let debug = false;; 
 let debug_print =
  fun msg -> if debug then prerr_endline (Lazy.force msg) else ()