[coqpp] [ltac] Adapt to removal of imperative proof state.

We add state handling to tactics.

TODO:

- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac

2 files changed, 16 insertions, 9 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index dc7d8ec1f0..07194578c1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -946,7 +946,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
       ignore (auto (Some prg.prg_name) None deps)
   end
 
-let rec solve_obligation ?ontop prg num tac =
+let rec solve_obligation ~ontop prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -972,14 +972,14 @@ let rec solve_obligation ?ontop prg num tac =
   let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in
   pstate
 
-and obligation ?ontop (user_num, name, typ) tac =
+and obligation ~ontop (user_num, name, typ) tac =
   let num = pred user_num in
   let prg = get_prog_err name in
   let obls, rem = prg.prg_obligations in
     if num >= 0 && num < Array.length obls then
       let obl = obls.(num) in
 	match obl.obl_body with
-          | None -> solve_obligation ?ontop prg num tac
+          | None -> solve_obligation ~ontop prg num tac
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
 
@@ -1179,7 +1179,7 @@ let admit_obligations n =
     let prg = get_prog_err n in
     admit_prog prg
 
-let next_obligation ?ontop n tac =
+let next_obligation ~ontop n tac =
   let prg = match n with
   | None -> get_any_prog_err ()
   | Some _ -> get_prog_err n
@@ -1190,7 +1190,7 @@ let next_obligation ?ontop n tac =
   | Some i -> i
   | None -> anomaly (Pp.str "Could not find a solvable obligation.")
   in
-  solve_obligation ?ontop prg i tac
+  solve_obligation ~ontop prg i tac
 
 let check_program_libraries () =
   Coqlib.check_required_library Coqlib.datatypes_module_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index eed3906a6a..b1b7b1ec90 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -85,10 +85,17 @@ val add_mutual_definitions :
   notations ->
   fixpoint_kind -> unit
 
-val obligation : ?ontop:Proof_global.t -> int * Names.Id.t option * Constrexpr.constr_expr option ->
-  Genarg.glob_generic_argument option -> Proof_global.t
-
-val next_obligation : ?ontop:Proof_global.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof_global.t
+val obligation
+  :  ontop:Proof_global.t option
+  -> int * Names.Id.t option * Constrexpr.constr_expr option
+  -> Genarg.glob_generic_argument option
+  -> Proof_global.t
+
+val next_obligation
+  :  ontop:Proof_global.t option
+  -> Names.Id.t option
+  -> Genarg.glob_generic_argument option
+  -> Proof_global.t
 
 val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)