please, commit files with debug=false otherwise the distributed matita prints a ton...

[helm.git] / components / tactics / destructTactic.ml

diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml
index 2ea9e047c79458d13c1975055c83161f6d7ffdef..1344e978fb0bafdf256fdec7593ddc257d842c2e 100644 (file)
--- a/components/tactics/destructTactic.ml
+++ b/components/tactics/destructTactic.ml
@@ -41,7 +41,7 @@ module ET = EqualityTactics
 module DTI = DoubleTypeInference
 module FNG = FreshNamesGenerator
 
-let debug = true
+let debug = false
 let debug_print = 
   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())