X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=6b25982d3bb7377b8a0a5019172e5f3f482ce678;hb=456ea05ac26bf48e4cdc0d745a92de0d14b3ff80;hp=09156224ec280e4d149486521af62895e52b9587;hpb=89be8e257ea6a9b7e30a595c8294e0972d165a72;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 09156224e..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
@@ -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 *)