]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/match_concl.ml
Corrections to "auto" tactic
[helm.git] / helm / ocaml / tactics / match_concl.ml
index 078cb931a903b26ac2281d6dd8fa7b4a0236fc78..c2266cd1004fbb0e4a2018ee3b7859e6843c4e32 100644 (file)
@@ -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
 ;;