- warn "in do_tactic";
- try
- let (proof, goallist) =
- if (n>0) then apply_tactic tactic status
- else apply_tactic id_tac status in
-(* else (proof, []) in *)
-(* perche' non va bene questo? stessa questione di ##### ? *)
- let rec step proof goallist =
- match goallist with
- [] -> (proof, [])
- | head::tail ->
- let (proof', goallist') =
- do_tactic ~n:(n-1) ~tactic (proof, head) in
- let (proof'', goallist'') = step proof' tail in
- proof'', goallist'@goallist''
- in
- step proof goallist
- with
- (Fail _) as e ->
- warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
- apply_tactic id_tac status
+ if n = 0 then
+ S.apply_tactic S.id_tac status
+ else
+ try
+ let output_status = S.apply_tactic tactic status in
+ let goallist = S.goals output_status in
+ let rec step output_status goallist =
+ match goallist with
+ [] -> output_status, []
+ | head::tail ->
+ let status = S.focus output_status head in
+ let output_status' = do_tactic ~n:(n-1) ~tactic status in
+ let goallist' = S.goals output_status' in
+ let (output_status'', goallist'') = step output_status' tail in
+ output_status'', goallist'@goallist''
+ in
+ let output_status,goals = step output_status goallist in
+ S.set_goals output_status goals
+ with
+ (Fail _) as e ->
+ warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+ S.apply_tactic S.id_tac status