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 (); *)
- (proof,[])
+ (match auto_new mqi_handle [(proof, [(goal,depth)])] with
+ | (proof,_)::_ ->
+ prerr_endline "AUTO_TAC HA FINITO";
+ (* CicMetaSubst.print_counters (); *)
+ (proof,[])
+ | _ -> assert false)
with
| NoOtherChoices ->
prerr_endline("Auto failed");