X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion.ml;h=fa4b71178a7886ba20c3ded480c323c0e4ea3b50;hb=d4b31ea5ca7c7dd3344cb284a89fac22312834cf;hp=13b350daf07f996a8142b177c3384bb59510c856;hpb=30743ffb0d331aaaa449957238128943ba781ecf;p=helm.git

diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml
index 13b350daf..fa4b71178 100644
--- 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 ()