X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fmatch_concl.ml;h=c2266cd1004fbb0e4a2018ee3b7859e6843c4e32;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=4f36f3ee55695705a025ee6927f2a49219834d73;hpb=5930f13b2d863abbff240ffa985bcc064c7a5ab8;p=helm.git

diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml
index 4f36f3ee5..c2266cd10 100644
--- a/helm/ocaml/tactics/match_concl.ml
+++ b/helm/ocaml/tactics/match_concl.ml
@@ -136,8 +136,9 @@ let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition)
 	     ("no_inconcl_aux.source = refObj0.source")::where) in
   let from = String.concat "," from in
   let where = String.concat " and " where in
-  let query = "select refObj0.source from " ^ from ^ " where " ^ where in
-    prerr_endline query;
+  let query = 
+        "select refObj0.source from " ^ from ^ " where " ^ where in
+   (* prerr_endline query;*)
     Mysql.exec conn query
 ;;
 
@@ -171,8 +172,10 @@ let cmatch (conn:Mysql.dbd) t =
     let prefixes = NewConstraints.prefixes just_factor t in
     (match prefixes with
 	 Some main, all_concl ->
+(*	 
            NewConstraints.pp_prefixes all_concl;
-	   (* in some cases, max_prefix_length could be less than n *)
+*)
+           (* in some cases, max_prefix_length could be less than n *)
 	   let max_prefix_length = 
 	     match all_concl with
 		 [] -> assert false