X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ffilter_auto.ml;h=73494c8e3414e43cc8eef6d376d99dd4f4fae735;hb=bb236c2ac110124de92fa2d0fb2882d273a7f7eb;hp=73eaed638c4aee767a317f4431c3bf246fefa774;hpb=16d6d961a5d7db08bfdf1bccae7f36c6b2fd7fe2;p=helm.git

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index 73eaed638..73494c8e3 100644
--- a/helm/ocaml/tactics/filter_auto.ml
+++ b/helm/ocaml/tactics/filter_auto.ml
@@ -41,7 +41,7 @@ let hyp_const (conn:Mysql.dbd) uri =
      "select h_occurrence from refObj where source='"^uri^
     "' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^
     "or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
-  prerr_endline ("$$$$$$$$$$$$$$$"^query);
+(*  prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
   let result = Mysql.exec conn query in 
   (* now we transform the result in a set *)
   let f a = 
@@ -59,7 +59,7 @@ let hyp_const (conn:Mysql.dbd) uri =
    const, the set of the costants of the proof *)
 let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
    let hyp = hyp_const conn uri in
-   prerr_endline (NewConstraints.pp_StringSet hyp);
+ (*  prerr_endline (NewConstraints.pp_StringSet hyp);*)
     NewConstraints.StringSet.subset hyp const
 ;;