Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.

4 files changed, 97 insertions, 60 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7333114eae..66b47a64a7 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_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
+let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
@@ -121,7 +121,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof ~ontop:None evd id goal_kind goals terminator in
+  let pf = Proof_global.start_proof evd id goal_kind goals terminator in
   try
     let pf, status = by tac pf in
     let open Proof_global in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 77d701b41f..ec52d2d5cf 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -23,17 +23,17 @@ exception NoSuchGoal
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
-val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
+val get_goal_context : Proof_global.pstate -> int -> Evd.evar_map * env
 
 (** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
+val get_current_goal_context : Proof_global.pstate -> Evd.evar_map * env
 
 (** [get_current_context ()] returns the context of the
   current focused goal. If there is no focused goal but there
   is a proof in progress, it returns the corresponding evar_map.
   If there is no pending proof then it returns the current global
   environment and empty evar_map. *)
-val get_current_context : Proof_global.t -> Evd.evar_map * env
+val get_current_context : Proof_global.pstate -> Evd.evar_map * env
 
 (** {6 ... } *)
 
@@ -49,7 +49,7 @@ val solve : ?with_end_tac:unit Proofview.tactic ->
     focused proof.
     Returns [false] if an unsafe tactic has been used. *)
 
-val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
+val by : unit Proofview.tactic -> Proof_global.pstate -> Proof_global.pstate * bool
 
 (** Option telling if unification heuristics should be used. *)
 val use_unification_heuristics : unit -> bool
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 40ae4acc88..8d7960829b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,23 +63,40 @@ let pstate_map f (pf, pfl) = (f pf, List.map f pfl)
 let make_terminator f = f
 let apply_terminator f = f
 
+let get_current_pstate (ps,_) = ps
+
 (* combinators for the current_proof lists *)
 let push ~ontop a =
   match ontop with
   | None -> a , []
   | Some (l,ls) -> a, (l :: ls)
 
+let maybe_push ~ontop = function
+  | Some pstate -> Some (push ~ontop pstate)
+  | None -> ontop
+
 (*** Proof Global manipulation ***)
 
 let get_all_proof_names (pf : t) =
   let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in
   pn :: pns
 
-let give_me_the_proof (ps,_) = ps.proof
-let get_current_proof_name (ps,_) = (Proof.data ps.proof).Proof.name
-let get_current_persistence (ps,_) = ps.strength
+let give_me_the_proof ps = ps.proof
+let get_current_proof_name ps = (Proof.data ps.proof).Proof.name
+let get_current_persistence ps = ps.strength
+
+let with_current_pstate f (ps,psl) =
+  let ps, ret = f ps in
+  (ps, psl), ret
+
+let modify_current_pstate f (ps,psl) =
+  f ps, psl
+
+let modify_proof f ps =
+  let proof = f ps.proof in
+  {ps with proof}
 
-let with_current_proof f (ps, psl) =
+let with_proof f ps =
   let et =
     match ps.endline_tactic with
     | None -> Proofview.tclUNIT ()
@@ -92,16 +109,23 @@ let with_current_proof f (ps, psl) =
   in
   let (newpr,ret) = f et ps.proof in
   let ps = { ps with proof = newpr } in
-  (ps, psl), ret
+  ps, ret
+
+let with_current_proof f (ps,rest) =
+  let ps, ret = with_proof f ps in
+  (ps, rest), ret
 
 let simple_with_current_proof f pf =
   let p, () = with_current_proof (fun t p -> f t p , ()) pf in p
 
-let compact_the_proof pf = simple_with_current_proof (fun _ -> Proof.compact) pf
+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
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac (ps, psl) =
-  { ps with endline_tactic = Some tac }, psl
+let set_endline_tactic tac ps =
+  { ps with endline_tactic = Some tac }
 
 let pf_name_eq id ps =
   let Proof.{ name } = Proof.data ps.proof in
@@ -112,8 +136,10 @@ let discard {CAst.loc;v=id} (ps, psl) =
   | [] -> None
   | ps :: psl -> Some (ps, psl)
 
-let discard_current (ps, psl) =
-  if List.is_empty psl then None else Some List.(hd psl, tl psl)
+let discard_current (_, psl) =
+  match psl with
+  | [] -> None
+  | ps :: psl -> Some (ps, psl)
 
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
@@ -123,30 +149,26 @@ let discard_current (ps, psl) =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof ~ontop sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
-  let initial_state = {
-    terminator = CEphemeron.create terminator;
+let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
+  { terminator = CEphemeron.create terminator;
     proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
     universe_decl = pl;
-    strength = kind } in
-  push ~ontop initial_state
+    strength = kind }
 
-let start_dependent_proof ~ontop name ?(pl=UState.default_univ_decl) kind goals terminator =
-  let initial_state = {
-    terminator = CEphemeron.create terminator;
+let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
+  { terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
     universe_decl = pl;
-    strength = kind } in
-  push ~ontop initial_state
+    strength = kind }
 
-let get_used_variables (pf,_) = pf.section_vars
-let get_universe_decl (pf,_) = pf.universe_decl
+let get_used_variables pf = pf.section_vars
+let get_universe_decl pf = pf.universe_decl
 
-let set_used_variables (ps,psl) l =
+let set_used_variables ps l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
@@ -170,9 +192,9 @@ let set_used_variables (ps,psl) l =
   if not (Option.is_empty ps.section_vars) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
   (* EJGA: This is always empty thus we should modify the type *)
-  (ctx, []), ({ ps with section_vars = Some ctx}, psl)
+  (ctx, []), { ps with section_vars = Some ctx}
 
-let get_open_goals (ps, _) =
+let get_open_goals ps =
   let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
   List.length goals +
   List.fold_left (+) 0
@@ -293,7 +315,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
-let return_proof ?(allow_partial=false) (ps,_) =
+let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
@@ -322,27 +344,27 @@ let return_proof ?(allow_partial=false) (ps,_) =
     List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
-let close_future_proof ~opaque ~feedback_id (ps, psl) proof =
+let close_future_proof ~opaque ~feedback_id ps proof =
   close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
 
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn (ps, psl) =
+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,psl))) ps
+    (Future.from_val ~fix_exn (return_proof ps)) ps
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator (ps, _) = CEphemeron.get ps.terminator
-let set_terminator hook (ps, psl) =
-  { ps with terminator = CEphemeron.create hook }, psl
+let get_terminator ps = CEphemeron.get ps.terminator
+let set_terminator hook ps =
+  { ps with terminator = CEphemeron.create hook }
 
 let copy_terminators ~src ~tgt =
   let (ps, psl), (ts,tsl) = src, tgt in
   assert(List.length psl = List.length tsl);
   {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
 
-let update_global_env (pf : t) =
+let update_global_env pf =
   let res, () =
-  with_current_proof (fun _ p ->
+  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
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e2e457483b..6984fff63a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -12,16 +12,20 @@
      toplevel. In particular it defines the global proof
      environment. *)
 
+type pstate
 type t
-val get_current_proof_name : t -> Names.Id.t
-val get_current_persistence : t -> Decl_kinds.goal_kind
+
+val get_current_pstate : t -> pstate
+
+val get_current_proof_name : pstate -> Names.Id.t
+val get_current_persistence : pstate -> Decl_kinds.goal_kind
 val get_all_proof_names : t -> Names.Id.t list
 
 val discard : Names.lident -> t -> t option
 val discard_current : t -> t option
 
-val give_me_the_proof : t -> Proof.t
-val compact_the_proof : t -> t
+val give_me_the_proof : pstate -> Proof.t
+val compact_the_proof : pstate -> pstate
 
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
@@ -52,6 +56,10 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
+val push : ontop:t option -> pstate -> t
+
+val maybe_push : ontop:t option -> pstate option -> t option
+
 (** [start_proof ~ontop id str pl goals terminator] starts a proof of name
    [id] with goals [goals] (a list of pairs of environment and
    conclusion); [str] describes what kind of theorem/definition this
@@ -60,25 +68,26 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
    morphism). The proof is started in the evar map [sigma] (which can
    typically contain universe constraints), and with universe bindings
    pl. *)
-val start_proof : ontop:t option ->
+val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
-    proof_terminator -> t
+    proof_terminator -> pstate
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
-val start_dependent_proof : ontop:t option ->
+val start_dependent_proof :
   Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
-  Proofview.telescope -> proof_terminator -> t
+  Proofview.telescope -> proof_terminator -> pstate
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
   there_are_pending_proofs. *)
-val update_global_env : t -> t
+val update_global_env : pstate -> pstate
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn ->
+  pstate -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -88,15 +97,15 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> t -> closed_proof_output
-val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
+val return_proof : ?allow_partial:bool -> pstate -> closed_proof_output
+val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> pstate ->
   closed_proof_output Future.computation -> closed_proof
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-val get_terminator : t -> proof_terminator
-val set_terminator : proof_terminator -> t -> t
-val get_open_goals : t -> int
+val get_terminator : pstate -> proof_terminator
+val set_terminator : proof_terminator -> pstate -> pstate
+val get_open_goals : pstate -> int
 
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
     no current proof.
@@ -106,18 +115,24 @@ val with_current_proof :
 val simple_with_current_proof :
   (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
 
+val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> pstate -> pstate * 'a
+val modify_proof : (Proof.t -> Proof.t) -> pstate -> pstate
+
+val with_current_pstate : (pstate -> pstate * 'a) -> t -> t * 'a
+val modify_current_pstate : (pstate -> pstate) -> t -> t
+
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
+val set_endline_tactic : Genarg.glob_generic_argument -> pstate -> pstate
 
 (** Sets the section variables assumed by the proof, returns its closure
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
-val set_used_variables : t ->
-  Names.Id.t list -> (Constr.named_context * Names.lident list) * t
+val set_used_variables : pstate ->
+  Names.Id.t list -> (Constr.named_context * Names.lident list) * pstate
 
-val get_used_variables : t -> Constr.named_context option
+val get_used_variables : pstate -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : t -> UState.universe_decl
+val get_universe_decl : pstate -> UState.universe_decl
 
 val copy_terminators : src:t -> tgt:t -> t