[proof] Uniformize Proof_global API

We rename modify to map [more in line with the rest of the system] and
make the endline function specific, as it is only used in one case.

5 files changed, 12 insertions, 26 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 160d933e50..4e346a9564 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -79,12 +79,6 @@ let get_terminator ps = ps.terminator
 
 end
 
-let with_proof f { proof; terminator } =
-  let proof, res = Proof_global.with_proof f proof in
-  { proof; terminator }, res
-
-let simple_with_proof f ps = fst @@ with_proof (fun t p -> f t p, ()) ps
-
 let by tac { proof; terminator } =
   let proof, res = Pfedit.by tac proof in
   { proof; terminator}, res
@@ -454,10 +448,10 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
       let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let lemma = simple_with_proof (fun _ p ->
+      let lemma = pf_map (Proof_global.map_proof (fun p ->
           match init_tac with
           | None -> p
-          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) lemma in
+          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma in
       lemma
 
 let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 9afcd9a7ce..ac647af8b5 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -70,16 +70,11 @@ val standard_proof_terminator
   -> proof_terminator
 
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
+val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
 val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
 
 val by : unit Proofview.tactic -> t -> t * bool
 
-val with_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
-
-val simple_with_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
-
 (* Start of high-level proofs with an associated constant *)
 
 val start_lemma
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 643d8ce1d6..d206165e88 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1162,7 +1162,7 @@ let focus_command_cond = Proof.no_cond command_focus
      all tactics fail if there are no further goals to prove. *)
 
 let vernac_solve_existential ~pstate n com =
-  Proof_global.modify_proof (fun p ->
+  Proof_global.map_proof (fun p ->
       let intern env sigma = Constrintern.intern_constr env sigma com in
       Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
@@ -2180,7 +2180,7 @@ let vernac_register qid r =
 (* Proof management *)
 
 let vernac_focus ~pstate gln =
-  Proof_global.modify_proof (fun p ->
+  Proof_global.map_proof (fun p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
@@ -2191,7 +2191,7 @@ let vernac_focus ~pstate gln =
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus ~pstate =
-  Proof_global.modify_proof
+  Proof_global.map_proof
     (fun p -> Proof.unfocus command_focus p ())
     pstate
 
@@ -2210,7 +2210,7 @@ let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
 let vernac_subproof gln ~pstate =
-  Proof_global.modify_proof (fun p ->
+  Proof_global.map_proof (fun p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
@@ -2220,12 +2220,12 @@ let vernac_subproof gln ~pstate =
     pstate
 
 let vernac_end_subproof ~pstate =
-  Proof_global.modify_proof (fun p ->
+  Proof_global.map_proof (fun p ->
       Proof.unfocus subproof_kind p ())
     pstate
 
 let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
-  Proof_global.modify_proof (fun p ->
+  Proof_global.map_proof (fun p ->
     Proof_bullet.put p bullet) pstate
 
 (* Stack is needed due to show proof names, should deprecate / remove
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index af68ef88cf..c51d3c30f4 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -121,12 +121,12 @@ module Proof_global = struct
   let give_me_the_proof () = cc get_proof
   let get_current_proof_name () = cc get_proof_name
 
-  let simple_with_current_proof f = dd (Proof_global.simple_with_proof f)
+  let map_proof f = dd (map_proof f)
   let with_current_proof f =
     match !s_lemmas with
     | None -> raise NoCurrentProof
     | Some stack ->
-      let pf, res = Stack.with_top_pstate stack ~f:(with_proof f) in
+      let pf, res = Stack.with_top_pstate stack ~f:(map_fold_proof_endline f) in
       let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in
       s_lemmas := Some stack;
       res
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index bfa85e022c..9f4e366e1c 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -45,13 +45,10 @@ module Proof_global : sig
   val give_me_the_proof_opt : unit -> Proof.t option
   val get_current_proof_name : unit -> Names.Id.t
 
-  val simple_with_current_proof :
-      (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
-
+  val map_proof : (Proof.t -> Proof.t) -> unit
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-
   val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
 
   type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator