[proof] Move proofs that have an associated constant to `Lemmas`

The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.

This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.

Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.

As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.

We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.

3 files changed, 62 insertions, 172 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c7fcc66120..00144e87dc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -42,11 +42,11 @@ let get_goal_context_gen pf i =
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
 let get_goal_context pf i =
-  let p = Proof_global.give_me_the_proof pf in
+  let p = Proof_global.get_proof pf in
   get_goal_context_gen p i
 
 let get_current_goal_context pf =
-  let p = Proof_global.give_me_the_proof pf in
+  let p = Proof_global.get_proof pf in
   try get_goal_context_gen p 1
   with
   | NoSuchGoal ->
@@ -57,7 +57,7 @@ let get_current_goal_context pf =
     Evd.from_env env, env
 
 let get_current_context pf =
-  let p = Proof_global.give_me_the_proof pf in
+  let p = Proof_global.get_proof pf in
   try get_goal_context_gen p 1
   with
   | NoSuchGoal ->
@@ -119,13 +119,12 @@ let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
   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 evd id goal_kind goals terminator in
+  let pf = Proof_global.start_proof evd id goal_kind goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
-    let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
+    let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
     match entries with
     | [entry] ->
       let univs = UState.demote_seff_univs entry universes in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b642e8eea7..f06b2885e2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,65 +36,20 @@ type proof_object = {
 
 type opacity_flag = Opaque | Transparent
 
-type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of opacity_flag *
-              lident option *
-              proof_object
-
-type proof_terminator = proof_ending -> unit
-type closed_proof = proof_object * proof_terminator
-
-type t = {
-  terminator : proof_terminator CEphemeron.key;
-  endline_tactic : Genarg.glob_generic_argument option;
-  section_vars : Constr.named_context option;
-  proof : Proof.t;
-  universe_decl: UState.universe_decl;
-  strength : Decl_kinds.goal_kind;
-}
-
-(* The head of [t] is the actual current proof, the other ones are
-   to be resumed when the current proof is closed or aborted. *)
-type stack = t * t list
-
-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
+type t =
+  { endline_tactic : Genarg.glob_generic_argument option
+  ; section_vars : Constr.named_context option
+  ; proof : Proof.t
+  ; universe_decl: UState.universe_decl
+  ; strength : Decl_kinds.goal_kind
+  }
 
 (*** Proof Global manipulation ***)
 
-let get_all_proof_names (pf : stack) =
-  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 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 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 et =
@@ -111,13 +66,6 @@ let with_proof f ps =
   let ps = { ps with proof = newpr } in
   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 simple_with_proof f ps =
   let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps
 
@@ -127,21 +75,7 @@ let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf
 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
-  Id.equal name id
-
-let discard {CAst.loc;v=id} (ps, psl) =
-  match List.filter (fun pf -> not (pf_name_eq id pf)) (ps :: psl) with
-  | [] -> None
-  | ps :: psl -> Some (ps, 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
+(** [start_proof sigma id pl str goals] 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
     is (spiwack: for potential printing, I believe is used only by
@@ -149,21 +83,21 @@ let discard_current (_, 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 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 }
-
-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 }
+let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals =
+  { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+  ; endline_tactic = None
+  ; section_vars = None
+  ; universe_decl = pl
+  ; strength = kind
+  }
+
+let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
+  { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+  ; endline_tactic = None
+  ; section_vars = None
+  ; universe_decl = pl
+  ; strength = kind
+  }
 
 let get_used_variables pf = pf.section_vars
 let get_universe_decl pf = pf.universe_decl
@@ -217,7 +151,7 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; terminator; universe_decl; strength } = ps in
+  let { section_vars; proof; universe_decl; strength } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -312,8 +246,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
   { id = name; entries = entries; persistence = strength;
-    universes },
-  fun pr_ending -> CEphemeron.get terminator pr_ending
+    universes }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
@@ -351,22 +284,11 @@ 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
 
-(** 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 =
-  { 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 =
   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
+        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
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index aff48b9636..84a833fb2c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,18 +13,16 @@
      environment. *)
 
 type t
-type stack
 
-val get_current_pstate : stack -> t
-
-val get_current_proof_name : t -> Names.Id.t
-val get_current_persistence : t -> Decl_kinds.goal_kind
-val get_all_proof_names : stack -> Names.Id.t list
+(* Should be moved into a proper view *)
+val get_proof : t -> Proof.t
+val get_proof_name : t -> Names.Id.t
+val get_persistence : t -> Decl_kinds.goal_kind
+val get_used_variables : t -> Constr.named_context option
 
-val discard : Names.lident -> stack -> stack option
-val discard_current : stack -> stack option
+(** Get the universe declaration associated to the current proof. *)
+val get_universe_decl : t -> UState.universe_decl
 
-val give_me_the_proof : t -> Proof.t
 val compact_the_proof : t -> t
 
 (** When a proof is closed, it is reified into a [proof_object], where
@@ -44,23 +42,7 @@ type proof_object = {
 
 type opacity_flag = Opaque | Transparent
 
-type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-                UState.t
-  | Proved of opacity_flag *
-              Names.lident option *
-              proof_object
-type proof_terminator
-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:stack option -> t -> stack
-
-val maybe_push : ontop:stack option -> t option -> stack option
-
-(** [start_proof ~ontop id str pl goals terminator] starts a proof of name
+(** [start_proof id str pl goals] 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
    is; [terminator] is used at the end of the proof to close the proof
@@ -68,16 +50,22 @@ val maybe_push : ontop:stack option -> t option -> stack option
    morphism). The proof is started in the evar map [sigma] (which can
    typically contain universe constraints), and with universe bindings
    pl. *)
-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
+val start_proof
+  :  Evd.evar_map
+  -> Names.Id.t
+  -> ?pl:UState.universe_decl
+  -> Decl_kinds.goal_kind
+  -> (Environ.env * EConstr.types) list
+  -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
-val start_dependent_proof :
-  Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
-  Proofview.telescope -> proof_terminator -> t
+val start_dependent_proof
+  :  Names.Id.t
+  -> ?pl:UState.universe_decl
+  -> Decl_kinds.goal_kind
+  -> Proofview.telescope
+  -> t
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
@@ -86,8 +74,7 @@ val update_global_env : t -> t
 
 (* 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 -> t -> proof_object
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -99,28 +86,17 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt
  * 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 ->
-  closed_proof_output Future.computation -> closed_proof
+  closed_proof_output Future.computation -> proof_object
 
-(** 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
 
 (** 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_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> stack -> stack * 'a
-val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t) -> stack -> stack
-
 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 with_current_pstate : (t -> t * 'a) -> stack -> stack * 'a
-val modify_current_pstate : (t -> t) -> stack -> stack
-
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 
@@ -129,10 +105,3 @@ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
  * ids to be cleared *)
 val set_used_variables : t ->
   Names.Id.t list -> (Constr.named_context * Names.lident list) * t
-
-val get_used_variables : t -> Constr.named_context option
-
-(** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : t -> UState.universe_decl
-
-val copy_terminators : src:stack -> tgt:stack -> stack