(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("TACTICALS WARNING: " ^ s)
+ debug_print ("TACTICALS WARNING: " ^ s)
(** TACTIC{,AL}S *)
| (Some (Cic.Name name,_))::_ when name = "T" -> n
| _::tl -> find (n+1) tl
in
- prerr_endline ("eseguo find");
+ debug_print ("eseguo find");
find 1 context
in
- prerr_endline ("eseguo apply");
+ debug_print ("eseguo apply");
apply_tac ~term:(Cic.Rel rel) status
in
(* do_tactic ~n:2 *)