removed some printings

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 09156224ec280e4d149486521af62895e52b9587..6b25982d3bb7377b8a0a5019172e5f3f482ce678 100644 (file)
--- 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
@@ -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 *)