[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.

13 files changed, 35 insertions, 55 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index cff8214438..79d1c7520f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -101,6 +101,6 @@ let start_deriving f suchthat name : Lemmas.t =
 
   let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
   let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
-  Lemmas.simple_with_proof begin fun _ p ->
+  Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-  end lemma
+  end) lemma
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0ded60d9c7..7691ca225e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -934,7 +934,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars STATE proof
 | [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -966,7 +966,7 @@ END
 VERNAC COMMAND EXTEND Unshelve STATE proof
 | [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Proof_global.map_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 960e5b76f8..d10d10a664 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.with_proof (fun etac p ->
+  let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info !print_info_trace in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 00144e87dc..5df223215d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
 
-let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
+let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac)
 
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f06b2885e2..8e1d16175f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -49,9 +49,11 @@ type t =
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
 let get_persistence ps = ps.strength
-let modify_proof f p = { p with proof = f p.proof }
 
-let with_proof f ps =
+let map_proof f p = { p with proof = f p.proof }
+let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
+
+let map_fold_proof_endline f ps =
   let et =
     match ps.endline_tactic with
     | None -> Proofview.tclUNIT ()
@@ -66,10 +68,7 @@ let with_proof f ps =
   let ps = { ps with proof = newpr } in
   ps, ret
 
-let simple_with_proof f ps =
-  let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps
-
-let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf
+let compact_the_proof pf = map_proof Proof.compact pf
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac ps =
@@ -284,11 +283,9 @@ let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
   close_proof ~opaque ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ps)) ps
 
-let update_global_env pf =
-  let res, () =
-  with_proof (fun _ p ->
-        Proof.in_proof p (fun sigma ->
-            let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-            let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in
-            (p, ()))) pf
-  in res
+let update_global_env =
+  map_proof (fun p ->
+      Proof.in_proof p (fun sigma ->
+          let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+          let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in
+          p))
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 84a833fb2c..fd0ad6fb50 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -90,12 +90,9 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
 
 val get_open_goals : t -> int
 
-(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
-    no current proof.
-    The return boolean is set to [false] if an unsafe tactic has been used. *)
-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
-val modify_proof : (Proof.t -> Proof.t) -> t -> t
+val map_proof : (Proof.t -> Proof.t) -> t -> t
+val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
+val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
diff --git a/stm/stm.ml b/stm/stm.ml
index 20ad645ec5..1e89d6937c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1940,7 +1940,7 @@ end = struct (* {{{ *)
            "goals only"))
        else begin
         let (i, ast) = r_ast in
-        PG_compat.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+        PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p);
         (* STATE SPEC:
          * - start : id
          * - return: id
@@ -1996,7 +1996,7 @@ end = struct (* {{{ *)
     stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
     TaskQueue.with_n_workers nworkers (fun queue ->
-    PG_compat.simple_with_current_proof (fun _ p ->
+    PG_compat.map_proof (fun p ->
       let Proof.{goals} = Proof.data p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 10dd1c4f58..3ab82b6e9b 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -856,7 +856,7 @@ let print_ltac qid =
 (** Calling tactics *)
 
 let solve ~pstate default tac =
-  let pstate, status = Proof_global.with_proof begin fun etac p ->
+  let pstate, status = Proof_global.map_fold_proof_endline begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
     let g = Goal_select.get_default_goal_selector () in
     let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
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