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

1 files changed, 24 insertions, 55 deletions

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