let auto_tac mqi_handle =
- CicMetaSubst.reset_counters ();
+(* CicMetaSubst.reset_counters (); *)
let auto_tac mqi_handle (proof,goal) =
prerr_endline "Entro in Auto";
try
let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
prerr_endline "AUTO_TAC HA FINITO";
- CicMetaSubst.print_counters ();
+(* CicMetaSubst.print_counters (); *)
(proof,[])
with
| NoOtherChoices ->