- match xostatus with
- | Some ostatus ->
- let opened,closed = S.goals ostatus in
- begin match opened with
- | [] -> ostatus
- | _ ->
- fold_eval (S.focus ~-1 ostatus)
- [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
- end
- | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
- )
-
-(* Tacticals that cannot be implemented on top of tynycals *)
+ let tactic = match xoutput with
+ | Some res -> then_ ~start:(const_tac res) ~continuation
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic if_