From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 22 Apr 2009 10:54:26 +0000 (+0000)
Subject: Disabled debug prints in the inversion principle.
X-Git-Tag: make_still_working~4062
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9dce41a62c86d55f2e9bb373bf9de0ec655b4f48;p=helm.git

Disabled debug prints in the inversion principle.
---

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 ()
 
diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index e15e8cb63..3229a261b 100644
--- 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 ()