]> matita.cs.unibo.it Git - helm.git/commitdiff
please, commit files with debug=false otherwise the distributed matita prints a ton...
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 8 Nov 2007 12:33:11 +0000 (12:33 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 8 Nov 2007 12:33:11 +0000 (12:33 +0000)
components/tactics/destructTactic.ml

index 2ea9e047c79458d13c1975055c83161f6d7ffdef..1344e978fb0bafdf256fdec7593ddc257d842c2e 100644 (file)
@@ -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 _ -> ())