X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=6afef50e050f2fb69a5f4e7ad0b9292f7cea9dd1;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=88f72ffa09d4d9b194f5f62b2eccbe67ce9882d4;hpb=3605d724ae0b95e17e668b6e140c35ab19568bb2;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 88f72ffa0..6afef50e0 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let debug_print = fun _ -> ()
+
 (* Da rimuovere, solo per debug*)
 let print_context ctx =
     let print_name =
@@ -106,9 +108,9 @@ let rec auto dbd = function
 	  Some (ey, ty) ->
             (* the goal is still there *)
             (*
-	    prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-	    prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-	    prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+	    debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+	    debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+	    debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
             *)
             (* if the goal contains metavariables we use the input
                signature for at_most constraints *)
@@ -156,12 +158,12 @@ let rec auto dbd = function
 
 let auto_tac  ?num ~(dbd:Mysql.dbd) =
   let auto_tac dbh (proof,goal) =
-  prerr_endline "Entro in Auto";
+  debug_print "Entro in Auto";
   match (auto dbd [(proof, [(goal,depth)],None)]) with
-      [] ->  prerr_endline("Auto failed");
+      [] ->  debug_print("Auto failed");
 	raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (proof,[],_)::_ ->  
-	prerr_endline "AUTO_TAC HA FINITO";
+	debug_print "AUTO_TAC HA FINITO";
 	(proof,[])
     | _ -> assert false
   in
@@ -335,8 +337,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
       match exitus with
 	  Yes (bo,_) ->
             (*
-              prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
-	      prerr_endline (CicPp.ppterm ty);
+              debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
+	      debug_print (CicPp.ppterm ty);
             *)
             let subst_in =
               (* if we just apply the subtitution, the type 
@@ -349,14 +351,14 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 		proof goal subst_in metasenv in
 	      [(subst_in,(proof,[],sign))]
         | No d when (d >= depth) -> 
-	    (* prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
+	    (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
 	    [] (* the empty list means no choices, i.e. failure *)
 	| No _ 
 	| NotYetInspected ->
              (*
-	      prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-	      prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-	      prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+	      debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+	      debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+	      debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
              *)
 	    let sign, new_sign =
 	      if is_meta_closed then
@@ -409,8 +411,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 			     in
 			       if not (cty = ty) then
 				 begin
-				   prerr_endline ("ty =  "^CicPp.ppterm ty);
-				   prerr_endline ("cty =  "^CicPp.ppterm cty);
+				   debug_print ("ty =  "^CicPp.ppterm ty);
+				   debug_print ("cty =  "^CicPp.ppterm cty);
 				   assert false
 				 end
 				   Hashtbl.add inspected_goals 
@@ -456,7 +458,7 @@ and auto_new_aux dbd width already_seen_goals = function
       let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in
       let len2 = List.length maxdepthgoals in
 	match maxdepthgoals with
-	  [] -> prerr_endline 
+	  [] -> debug_print 
 	    ("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth);
 	    auto_new dbd 
 	      width already_seen_goals((subst,(proof, othergoals, sign))::tl) 
@@ -492,7 +494,7 @@ and auto_new_aux dbd width already_seen_goals = function
 			auto_new dbd width already_seen_goals all_choices 
 		  | _ -> assert false
 	    end
-	  | None -> prerr_endline "caso none";
+	  | None -> debug_print "caso none";
 	      auto_new 
 		dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
 	      end
@@ -502,15 +504,15 @@ and auto_new_aux dbd width already_seen_goals = function
 let auto_tac_new  ~(dbd:Mysql.dbd) =
   let auto_tac dbd (proof,goal) =
   Hashtbl.clear inspected_goals;
-  prerr_endline "Entro in Auto";
+  debug_print "Entro in Auto";
   let id t = t in
   match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
-      [] ->  prerr_endline("Auto failed");
+      [] ->  debug_print("Auto failed");
 	raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (_,(proof,[],_))::_ ->  
-	prerr_endline "AUTO_TAC HA FINITO";
+	debug_print "AUTO_TAC HA FINITO";
 	let _,_,p,_ = proof in
-	prerr_endline (CicPp.ppterm p);
+	debug_print (CicPp.ppterm p);
 	(proof,[])
     | _ -> assert false
   in