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

3 files changed, 15 insertions, 21 deletions

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