X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=6b25982d3bb7377b8a0a5019172e5f3f482ce678;hb=0080faad4e730c227b6bbb2549407b23703b477a;hp=e7c11d43dfc9371613085d3ff2081562bdcccbb6;hpb=8e76ac2823de8cffc0b5f75b36264f86e3d0b52d;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index e7c11d43d..6b25982d3 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1,4 +1,5 @@
 (* Copyright (C) 2002, HELM Team.
+
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -26,7 +27,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = true;;
+let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
@@ -182,13 +183,17 @@ let only signature context metasenv t =
     in
     let consts = MetadataConstraints.constants_of ty in
     let b = MetadataConstraints.UriManagerSet.subset consts signature in
-    if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b) 
+(*     if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b)  *)
+    if b then b 
     else
       let ty' = unfold context ty in
       let consts' = MetadataConstraints.constants_of ty' in
       let b = MetadataConstraints.UriManagerSet.subset consts' signature  in
+(*
 	if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t))
-	else prerr_endline ("keeping " ^ (CicPp.ppterm t)); b
+	else prerr_endline ("keeping " ^ (CicPp.ppterm t)); 
+*)
+      b
   with 
   | CicTypeChecker.TypeCheckerFailure _ -> assert false
   | ProofEngineTypes.Fail _ -> false (* unfold may fail *)