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

15 files changed, 423 insertions, 260 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ed207b52dd..b64af52b6e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -378,11 +378,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
-  let pstate = Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+  let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
       ~hook:(Lemmas.mk_hook
                (fun _ _ _ -> instance_hook pri global imps ?hook)) in
   (* spiwack: I don't know what to do with the status here. *)
-  let pstate =
+  let lemma =
     if not (Option.is_empty term) then
       let init_refine =
         Tacticals.New.tclTHENLIST [
@@ -391,18 +391,18 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
           Tactics.New.reduce_after_refine;
         ]
       in
-      let pstate, _ = Pfedit.by init_refine pstate in
-      pstate
+      let lemma, _ = Lemmas.by init_refine lemma in
+      lemma
     else
-      let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
-      pstate
+      let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in
+      lemma
   in
   match tac with
   | Some tac ->
-    let pstate, _ = Pfedit.by tac pstate in
-    pstate
+    let lemma, _ = Lemmas.by tac lemma in
+    lemma
   | None ->
-    pstate
+    lemma
 
 let do_instance_subst_constructor_and_ty subst k u ctx =
   let subst =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e61935c87a..ace9096469 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -31,8 +31,8 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
 val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
-val new_instance_interactive :
-  ?global:bool (** Not global by default. *)
+val new_instance_interactive
+  :  ?global:bool (** Not global by default. *)
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
@@ -41,10 +41,10 @@ val new_instance_interactive :
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
-  -> Id.t * Proof_global.t
+  -> Id.t * Lemmas.t
 
-val new_instance :
-  ?global:bool (** Not global by default. *)
+val new_instance
+  :  ?global:bool (** Not global by default. *)
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
@@ -55,8 +55,8 @@ val new_instance :
   -> Hints.hint_info_expr
   -> Id.t
 
-val new_instance_program :
-  ?global:bool (** Not global by default. *)
+val new_instance_program
+  : ?global:bool (** Not global by default. *)
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index fa4860b079..c3575594b6 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -33,7 +33,13 @@ val do_definition
 (************************************************************************)
 
 (** Not used anywhere. *)
-val interp_definition : program_mode:bool ->
-  universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
-  constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
-                        UState.universe_decl * Impargs.manual_implicits
+val interp_definition
+  :  program_mode:bool
+  -> universe_decl_expr option
+  -> local_binder_expr list
+  -> polymorphic
+  -> red_expr option
+  -> constr_expr
+  -> constr_expr option
+  -> Safe_typing.private_constants definition_entry *
+     Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index fd88c6c4ad..3a25cb496c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -267,10 +267,10 @@ let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),p
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
       fixdefs) in
   let evd = Evd.from_ctx ctx in
-  let pstate = Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
+  let lemma = Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody Fixpoint)
     evd pl (Some(false,indexes,init_tac)) thms None in
   declare_fixpoint_notations ntns;
-  pstate
+  lemma
 
 let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   (* We shortcut the proof process *)
@@ -304,11 +304,11 @@ let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes)
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
       fixdefs) in
   let evd = Evd.from_ctx ctx in
-  let pstate = Lemmas.start_proof_with_initialization
+  let lemma = Lemmas.start_lemma_with_initialization
     (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint)
     evd pl (Some(true,[],init_tac)) thms None in
   declare_cofixpoint_notations ntns;
-  pstate
+  lemma
 
 let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   (* We shortcut the proof process *)
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index c8d617da5f..a31f3c34e0 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,13 +19,13 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_fixpoint :
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint_interactive :
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_cofixpoint :
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7de6d28560..7e70de4209 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -26,7 +26,6 @@ open Decl_kinds
 open Declare
 open Pretyping
 open Termops
-open Namegen
 open Reductionops
 open Constrintern
 open Impargs
@@ -46,6 +45,46 @@ let call_hook ?hook ?fix_exn uctx trans l c =
     let e = Option.cata (fun fix -> fix e) e fix_exn in
     iraise e
 
+(* Support for terminators and proofs with an associated constant
+   [that can be saved] *)
+
+type proof_ending =
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
+  | Proved of Proof_global.opacity_flag *
+              lident option *
+              Proof_global.proof_object
+
+type proof_terminator = proof_ending -> unit
+
+let make_terminator f = f
+let apply_terminator f = f
+
+(* Proofs with a save constant function *)
+type t =
+  { proof : Proof_global.t
+  ; terminator : proof_terminator CEphemeron.key
+  }
+
+let pf_map f { proof; terminator} = { proof = f proof; terminator }
+let pf_fold f ps = f ps.proof
+
+let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
+
+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
+
+(** 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 }
+
 (* Support for mutually proved theorems *)
 
 let retrieve_first_recthm uctx = function
@@ -203,9 +242,6 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
 
 let default_thm_id = Id.of_string "Unnamed_thm"
 
-let fresh_name_for_anonymous_theorem () =
-  next_global_ident_away default_thm_id Id.Set.empty
-
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
@@ -265,7 +301,6 @@ let check_anonymity id save_ident =
     user_err Pp.(str "This command can only be used for unnamed theorem.")
 
 (* Admitted *)
-
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
                    (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
@@ -312,7 +347,41 @@ let initialize_named_context_for_proof () =
       let d = if variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+module Stack = struct
+
+  type lemma = t
+  type nonrec t = t * t list
+
+  let map f (pf, pfl) = (f pf, List.map f pfl)
+
+  let map_top ~f (pf, pfl) = (f pf, pfl)
+  let map_top_pstate ~f (pf, pfl) = (pf_map f pf, pfl)
+
+  let pop (ps, p) = match p with
+    | [] -> ps, None
+    | pp :: p -> ps, Some (pp, p)
+
+  let with_top (p, _) ~f = f p
+  let with_top_pstate (p, _) ~f = f p.proof
+
+  let push ontop a =
+    match ontop with
+    | None -> a , []
+    | Some (l,ls) -> a, (l :: ls)
+
+  let get_all_proof_names (pf : t) =
+    let prj x = Proof_global.get_proof x in
+    let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in
+    pn :: pns
+
+  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
+
+end
+
+let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
   let terminator = match terminator with
   | None -> standard_proof_terminator ?hook compute_guard
   | Some terminator -> terminator ?hook compute_guard
@@ -323,7 +392,18 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
     | None -> initialize_named_context_for_proof ()
   in
   let goals = [ Global.env_of_context sign , c ] in
-  Proof_global.start_proof sigma id ?pl kind goals terminator
+  let proof = Proof_global.start_proof sigma id ?pl kind goals in
+  let terminator = CEphemeron.create terminator in
+  { proof ; terminator }
+
+let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
+  let terminator = match terminator with
+  | None -> standard_proof_terminator ?hook compute_guard
+  | Some terminator -> terminator ?hook compute_guard
+  in
+  let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
+  let terminator = CEphemeron.create terminator in
+  { proof ; terminator }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -339,7 +419,7 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
+let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
   let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
@@ -371,14 +451,14 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
         List.iter (fun (ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
-      let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let pstate = Proof_global.modify_proof (fun p ->
+      let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+      let lemma = simple_with_proof (fun _ p ->
           match init_tac with
           | None -> p
-          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
-      pstate
+          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) lemma in
+      lemma
 
-let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
+let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
   let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -410,7 +490,7 @@ let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  start_proof_with_initialization ?hook kind evd decl recguard thms snl
+  start_lemma_with_initialization ?hook kind evd decl recguard thms snl
 
 (* Saving a proof *)
 
@@ -425,7 +505,7 @@ let () =
       optread  = (fun () -> !keep_admitted_vars);
       optwrite = (fun b -> keep_admitted_vars := b) }
 
-let save_proof_admitted ?proof ~pstate =
+let save_lemma_admitted ?proof ~(lemma : t) =
   let pe =
     let open Proof_global in
     match proof with
@@ -440,8 +520,8 @@ let save_proof_admitted ?proof ~pstate =
       let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
       Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
     | None ->
-      let pftree = Proof_global.give_me_the_proof pstate in
-      let gk = Proof_global.get_current_persistence pstate in
+      let pftree = Proof_global.get_proof lemma.proof in
+      let gk = Proof_global.get_persistence lemma.proof in
       let Proof.{ name; poly; entry } = Proof.data pftree in
       let typ = match Proofview.initial_goals entry with
         | [typ] -> snd typ
@@ -453,10 +533,10 @@ let save_proof_admitted ?proof ~pstate =
       let universes = Proof.((data pftree).initial_euctx) in
       (* This will warn if the proof is complete *)
       let pproofs, _univs =
-        Proof_global.return_proof ~allow_partial:true pstate in
+        Proof_global.return_proof ~allow_partial:true lemma.proof in
       let sec_vars =
         if not !keep_admitted_vars then None
-        else match Proof_global.get_used_variables pstate, pproofs with
+        else match Proof_global.get_used_variables lemma.proof, pproofs with
           | Some _ as x, _ -> x
           | None, (pproof, _) :: _ ->
             let env = Global.env () in
@@ -464,32 +544,23 @@ let save_proof_admitted ?proof ~pstate =
             let ids_def = Environ.global_vars_set env pproof in
             Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
           | _ -> None in
-      let decl = Proof_global.get_universe_decl pstate in
+      let decl = Proof_global.get_universe_decl lemma.proof in
       let ctx = UState.check_univ_decl ~poly universes decl in
       Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
   in
-  Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
-
-let save_pstate_proved ~pstate ~opaque ~idopt =
-  let obj, terminator = Proof_global.close_proof ~opaque
-      ~keep_body_ucst_separate:false (fun x -> x) pstate
-  in
-  Proof_global.(apply_terminator terminator (Proved (opaque, idopt, obj)))
+  CEphemeron.get lemma.terminator pe
 
-let save_proof_proved ?proof ?ontop ~opaque ~idopt =
+let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   (* Invariant (uh) *)
-  if Option.is_empty ontop && Option.is_empty proof then
+  if Option.is_empty lemma && Option.is_empty proof then
     user_err (str "No focused proof (No proof-editing in progress).");
   let (proof_obj,terminator) =
     match proof with
     | None ->
       (* XXX: The close_proof and proof state API should be refactored
          so it is possible to insert proofs properly into the state *)
-      let pstate = Proof_global.get_current_pstate @@ Option.get ontop in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate
+      let { proof; terminator } = Option.get lemma in
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, CEphemeron.get terminator
     | Some proof -> proof
   in
-  (* if the proof is given explicitly, nothing has to be deleted *)
-  let ontop = if Option.is_empty proof then Proof_global.discard_current Option.(get ontop) else ontop in
-  Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
-  ontop
+  terminator (Proved (opaque,idopt,proof_obj))
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 3df543156d..2c51095786 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,6 +11,7 @@
 open Names
 open Decl_kinds
 
+(* Declaration hooks *)
 type declaration_hook
 
 (* Hooks allow users of the API to perform arbitrary actions at
@@ -37,53 +38,118 @@ val call_hook
   -> ?fix_exn:Future.fix_exn
   -> hook_type
 
-val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
-  ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val ->
-  ?compute_guard:Proof_global.lemma_possible_guards ->
-  ?hook:declaration_hook -> EConstr.types -> Proof_global.t
+(* Proofs that define a constant + terminators *)
+type t
+type proof_terminator
 
-val start_proof_com
+module Stack : sig
+
+  type lemma = t
+  type t
+
+  val pop : t -> lemma * t option
+  val push : t option -> lemma -> t
+
+  val map_top : f:(lemma -> lemma) -> t -> t
+  val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t
+
+  val with_top : t -> f:(lemma -> 'a ) -> 'a
+  val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a
+
+  val get_all_proof_names : t -> Names.Id.t list
+
+  val copy_terminators : src:t -> tgt:t -> t
+  (** Gets the current terminator without checking that the proof has
+      been completed. Useful for the likes of [Admitted]. *)
+
+end
+
+val standard_proof_terminator
+  :  ?hook:declaration_hook
+  -> Proof_global.lemma_possible_guards
+  -> proof_terminator
+
+val set_endline_tactic : Genarg.glob_generic_argument -> 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
+  :  Id.t
+  -> ?pl:UState.universe_decl
+  -> goal_kind
+  -> Evd.evar_map
+  -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?sign:Environ.named_context_val
+  -> ?compute_guard:Proof_global.lemma_possible_guards
+  -> ?hook:declaration_hook
+  -> EConstr.types
+  -> t
+
+val start_dependent_lemma
+  :  Id.t
+  -> ?pl:UState.universe_decl
+  -> goal_kind
+  -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?sign:Environ.named_context_val
+  -> ?compute_guard:Proof_global.lemma_possible_guards
+  -> ?hook:declaration_hook
+  -> Proofview.telescope
+  -> t
+
+val start_lemma_com
   :  program_mode:bool
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
-  -> Proof_global.t
-
-val start_proof_with_initialization :
-  ?hook:declaration_hook ->
-  goal_kind -> Evd.evar_map -> UState.universe_decl ->
-  (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
-  (Id.t (* name of thm *) *
-     (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-  -> int list option -> Proof_global.t
+  -> t
 
-val standard_proof_terminator :
-  ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
-  Proof_global.proof_terminator
+val start_lemma_with_initialization
+  :  ?hook:declaration_hook
+  -> goal_kind -> Evd.evar_map -> UState.universe_decl
+  -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
+  -> (Id.t (* name of thm *) *
+     (EConstr.types (* type of thm *) *
+      (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+  -> int list option
+  -> t
 
-val fresh_name_for_anonymous_theorem : unit -> Id.t
+val default_thm_id : Names.Id.t
 
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
 
 val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
-(** {6 ... } *)
+(** {6 Saving proofs } *)
 
-val save_proof_admitted
-  :  ?proof:Proof_global.closed_proof
-  -> pstate:Proof_global.t
+val save_lemma_admitted
+  :  ?proof:(Proof_global.proof_object * proof_terminator)
+  -> lemma:t
   -> unit
 
-val save_proof_proved
-  :  ?proof:Proof_global.closed_proof
-  -> ?ontop:Proof_global.stack
-  -> opaque:Proof_global.opacity_flag
-  -> idopt:Names.lident option
-  -> Proof_global.stack option
-
-val save_pstate_proved
-  : pstate:Proof_global.t
+val save_lemma_proved
+  :  ?proof:(Proof_global.proof_object * proof_terminator)
+  -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
+
+(* API to build a terminator, should go away *)
+type proof_ending =
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
+  | Proved of Proof_global.opacity_flag *
+              Names.lident option *
+              Proof_global.proof_object
+
+val make_terminator : (proof_ending -> unit) -> proof_terminator
+val apply_terminator : proof_terminator -> proof_ending -> unit
+val get_terminator : t -> proof_terminator
+val set_terminator : proof_terminator -> t -> t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 36cf9e0a31..f1286e2f1f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -841,7 +841,8 @@ let solve_by_tac ?loc name evi t poly ctx =
 
 let obligation_terminator ?hook name num guard auto pf =
   let open Proof_global in
-  let term = Lemmas.standard_proof_terminator ?hook guard in
+  let open Lemmas in
+  let term = standard_proof_terminator ?hook guard in
   match pf with
   | Admitted _ -> apply_terminator term pf
   | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
@@ -964,13 +965,13 @@ let rec solve_obligation prg num tac =
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
   let terminator ?hook guard =
-    Proof_global.make_terminator
+    Lemmas.make_terminator
       (obligation_terminator prg.prg_name num guard ?hook auto) in
   let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
-  let pstate = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
-  let pstate = fst @@ Pfedit.by !default_tactic pstate in
-  let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in
-  pstate
+  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
+  let lemma = fst @@ Lemmas.by !default_tactic lemma in
+  let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
+  lemma
 
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 3b77039de5..8734d82970 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -86,14 +86,14 @@ val add_mutual_definitions :
   fixpoint_kind -> unit
 
 val obligation
-  : int * Names.Id.t option * Constrexpr.constr_expr option
+  :  int * Names.Id.t option * Constrexpr.constr_expr option
   -> Genarg.glob_generic_argument option
-  -> Proof_global.t
+  -> Lemmas.t
 
 val next_obligation
-  : Names.Id.t option
+  :  Names.Id.t option
   -> Genarg.glob_generic_argument option
-  -> Proof_global.t
+  -> Lemmas.t
 
 val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4f66f2b790..643d8ce1d6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -38,28 +38,24 @@ module NamedDecl = Context.Named.Declaration
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
+
 (* XXX Should move to a common library *)
 let vernac_pperr_endline pp =
   if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
 
-(* Misc *)
-
-let there_are_pending_proofs ~pstate =
-  not Option.(is_empty pstate)
+(* Utility functions, at some point they should all disappear and
+   instead enviroment/state selection should be done at the Vernac DSL
+   level. *)
 
-(* EJGA: Only used in close_proof 2, can remove once ?proof hack is away *)
-let vernac_require_open_proof ~pstate f =
-  match pstate with
-  | Some pstate -> f ~pstate
+(* EJGA: Only used in close_proof, can remove once the ?proof hack is no more *)
+let vernac_require_open_lemma ~stack f =
+  match stack with
+  | Some stack -> f ~stack
   | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
 
-let with_pstate ~pstate f =
-  vernac_require_open_proof ~pstate
-    (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate))
-
- let modify_pstate ~pstate f =
-   vernac_require_open_proof ~pstate (fun ~pstate ->
-       Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
+let with_pstate ~stack f =
+  vernac_require_open_lemma ~stack
+    (fun ~stack -> Stack.with_top_pstate stack ~f:(fun pstate -> f ~pstate))
 
 let get_current_or_global_context ~pstate =
   match pstate with
@@ -122,7 +118,7 @@ let show_proof ~pstate =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   try
     let pstate = Option.get pstate in
-    let p = Proof_global.give_me_the_proof pstate in
+    let p = Proof_global.get_proof pstate in
     let sigma, env = Pfedit.get_current_context pstate in
     let pprf = Proof.partial_proof p in
     Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
@@ -132,24 +128,21 @@ let show_proof ~pstate =
   | Option.IsNone ->
     user_err (str "No goals to show.")
 
-let show_top_evars ~pstate =
+let show_top_evars ~proof =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
-  let pfts = Proof_global.give_me_the_proof pstate in
-  let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in
+  let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in
   pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
 
-let show_universes ~pstate =
-  let pfts = Proof_global.give_me_the_proof pstate in
-  let Proof.{goals;sigma} = Proof.data pfts in
+let show_universes ~proof =
+  let Proof.{goals;sigma} = Proof.data proof in
   let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
   Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
   str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx
 
 (* Simulate the Intro(s) tactic *)
-let show_intro ~pstate all =
+let show_intro ~proof all =
   let open EConstr in
-  let pf = Proof_global.give_me_the_proof pstate in
-  let Proof.{goals;sigma} = Proof.data pf in
+  let Proof.{goals;sigma} = Proof.data proof in
   if not (List.is_empty goals) then begin
     let gl = {Evd.it=List.hd goals ; sigma = sigma; } in
     let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
@@ -586,7 +579,7 @@ let start_proof_and_print ~program_mode ?hook k l =
       in Some hook
     else None
   in
-  start_proof_com ~program_mode ?inference_hook ?hook k l
+  start_lemma_com ~program_mode ?inference_hook ?hook k l
 
 let vernac_definition_hook p = function
 | Coercion ->
@@ -597,6 +590,9 @@ let vernac_definition_hook p = function
   Some (Class.add_subclass_hook p)
 | _ -> None
 
+let fresh_name_for_anonymous_theorem () =
+  Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty
+
 let vernac_definition_name lid local =
   let lid =
     match lid with
@@ -641,18 +637,27 @@ let vernac_start_proof ~atts kind l =
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
   start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
 
-let vernac_end_proof ?pstate:ontop ?proof = function
+let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
   | Admitted ->
-    with_pstate ~pstate:ontop (save_proof_admitted ?proof);
-    ontop
+    vernac_require_open_lemma ~stack (fun ~stack ->
+      let lemma, stack = Stack.pop stack in
+      save_lemma_admitted ?proof ~lemma;
+      stack)
   | Proved (opaque,idopt) ->
-    save_proof_proved ?ontop ?proof ~opaque ~idopt
+    let lemma, stack = match stack with
+      | None -> None, None
+      | Some stack ->
+        let lemma, stack = Stack.pop stack in
+        Some lemma, stack
+    in
+    save_lemma_proved ?lemma ?proof ~opaque ~idopt;
+    stack
 
-let vernac_exact_proof ~pstate c =
+let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
-  let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
-  let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
+  let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
+  let () = save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -1167,15 +1172,14 @@ let vernac_set_end_tac ~pstate tac =
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
   Proof_global.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
+let vernac_set_used_variables ~pstate e : Proof_global.t =
   let env = Global.env () in
   let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
-  let tys =
-    List.map snd (initial_goals (Proof_global.give_me_the_proof pstate)) in
+  let tys = List.map snd (initial_goals (Proof_global.get_proof pstate)) in
   let tys = List.map EConstr.Unsafe.to_constr tys in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
-  List.iter (fun id -> 
+  List.iter (fun id ->
     if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
       user_err ~hdr:"vernac_set_used_variables"
         (str "Unknown variable: " ++ Id.print id))
@@ -1878,10 +1882,10 @@ let get_current_context_of_args ~pstate =
   match pstate with
   | None -> fun _ ->
     let env = Global.env () in Evd.(from_env env, env)
-  | Some pstate ->
+  | Some lemma ->
     function
-    | Some n -> Pfedit.get_goal_context pstate n
-    | None -> Pfedit.get_current_context pstate
+    | Some n -> Pfedit.get_goal_context lemma n
+    | None -> Pfedit.get_current_context lemma
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1946,7 +1950,7 @@ let vernac_global_check c =
 
 
 let get_nth_goal ~pstate n =
-  let pf = Proof_global.give_me_the_proof pstate in
+  let pf = Proof_global.get_proof pstate in
   let Proof.{goals;sigma} = Proof.data pf in
   let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
@@ -2022,9 +2026,9 @@ let vernac_print ~pstate ~atts =
   | PrintHintGoal ->
      begin match pstate with
      | Some pstate ->
-        Hints.pr_applicable_hint pstate
+       Hints.pr_applicable_hint pstate
      | None ->
-        str "No proof in progress"
+       str "No proof in progress"
      end
   | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
   | PrintHintDb -> Hints.pr_searchtable env sigma
@@ -2193,13 +2197,12 @@ let vernac_unfocus ~pstate =
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused ~pstate =
-  let p = Proof_global.give_me_the_proof pstate in
+  let p = Proof_global.get_proof pstate in
   if Proof.unfocused p then
     str"The proof is indeed fully unfocused."
   else
     user_err Pp.(str "The proof is not fully unfocused.")
 
-
 (* "{" focuses on the first goal, "n: {" focuses on the n-th goal
     "}" unfocuses, provided that the proof of the goal has been completed.
 *)
@@ -2239,25 +2242,26 @@ let vernac_show ~pstate =
     end
   (* Show functions that require a proof state *)
   | Some pstate ->
+    let proof = Proof_global.get_proof pstate in
     begin function
     | ShowGoal goalref ->
-      let proof = Proof_global.give_me_the_proof pstate in
       begin match goalref with
         | OpenSubgoals -> pr_open_subgoals ~proof
         | NthGoal n -> pr_nth_open_subgoal ~proof n
         | GoalId id -> pr_goal_by_id ~proof id
       end
-    | ShowExistentials -> show_top_evars ~pstate
-    | ShowUniverses -> show_universes ~pstate
+    | ShowExistentials -> show_top_evars ~proof
+    | ShowUniverses -> show_universes ~proof
+    (* Deprecate *)
     | ShowProofNames ->
-      Id.print (Proof_global.get_current_proof_name pstate)
-    | ShowIntros all -> show_intro ~pstate all
+      Id.print (Proof_global.get_proof_name pstate)
+    | ShowIntros all -> show_intro ~proof all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
     end
 
 let vernac_check_guard ~pstate =
-  let pts = Proof_global.give_me_the_proof pstate in
+  let pts = Proof_global.get_proof pstate in
   let pfterm = List.hd (Proof.partial_proof pts) in
   let message =
     try
@@ -2322,30 +2326,31 @@ let locate_if_not_already ?loc (e, info) =
 
 exception End_of_input
 
-let interp_typed_vernac c ~pstate =
-  let open Proof_global in
+let interp_typed_vernac c ~stack =
   let open Vernacextend in
   match c with
-  | VtDefault f -> f (); pstate
+  | VtDefault f -> f (); stack
   | VtNoProof f ->
-    if there_are_pending_proofs ~pstate then
+    if Option.has_some stack then
       user_err Pp.(str "Command not supported (Open proofs remain)");
     let () = f () in
-    pstate
+    stack
   | VtCloseProof f ->
-    vernac_require_open_proof ~pstate (fun ~pstate ->
-        f ~pstate:(Proof_global.get_current_pstate pstate);
-        Proof_global.discard_current pstate)
+    vernac_require_open_lemma ~stack (fun ~stack ->
+        let lemma, stack = Stack.pop stack in
+        f ~lemma;
+        stack)
   | VtOpenProof f ->
-    Some (push ~ontop:pstate (f ()))
+    Some (Stack.push stack (f ()))
   | VtModifyProof f ->
-    modify_pstate f ~pstate
+    Option.map (Stack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
   | VtReadProofOpt f ->
-    f ~pstate:(Option.map get_current_pstate pstate);
-    pstate
+    let pstate = Option.map (Stack.with_top_pstate ~f:(fun x -> x)) stack in
+    f ~pstate;
+    stack
   | VtReadProof f ->
-    with_pstate ~pstate f;
-    pstate
+    with_pstate ~stack f;
+    stack
 
 (* We interpret vernacular commands to a DSL that specifies their
    allowed actions on proof states *)
@@ -2398,9 +2403,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacStartTheoremProof (k,l) ->
     VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l)
   | VernacExactProof c ->
-    VtCloseProof(fun ~pstate ->
+    VtCloseProof (fun ~lemma ->
         unsupported_attributes atts;
-        vernac_exact_proof ~pstate c)
+        vernac_exact_proof ~lemma c)
 
   | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
     let i () =
@@ -2671,7 +2676,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let rec interp_expr ?proof ~atts ~st c =
-  let pstate = st.Vernacstate.proof in
+  let stack = st.Vernacstate.lemmas in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
@@ -2699,11 +2704,11 @@ let rec interp_expr ?proof ~atts ~st c =
   (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *)
   | VernacEndProof e ->
     unsupported_attributes atts;
-    vernac_end_proof ?proof ?pstate e
+    vernac_end_proof ?proof ?stack e
 
   | v ->
     let fv = translate_vernac ~atts v in
-    interp_typed_vernac ~pstate fv
+    interp_typed_vernac ~stack fv
 
 (* XXX: This won't properly set the proof mode, as of today, it is
    controlled by the STM. Thus, we would need access information from
@@ -2712,8 +2717,9 @@ let rec interp_expr ?proof ~atts ~st c =
    without a considerable amount of refactoring.
  *)
 and vernac_load ~verbosely ~st fname =
-  let pstate = st.Vernacstate.proof in
-  if there_are_pending_proofs ~pstate then
+  let there_are_pending_proofs ~stack = not Option.(is_empty stack) in
+  let stack = st.Vernacstate.lemmas in
+  if there_are_pending_proofs ~stack then
     CErrors.user_err Pp.(str "Load is not supported inside proofs.");
   (* Open the file *)
   let fname =
@@ -2730,29 +2736,29 @@ and vernac_load ~verbosely ~st fname =
     match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
       | Some x -> x
       | None -> raise End_of_input) in
-  let rec load_loop ~pstate =
+  let rec load_loop ~stack =
     try
-      let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in
-      let pstate =
-        v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.proof = pstate })
+      let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
+      let stack =
+        v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack })
           (parse_sentence proof_mode input) in
-      load_loop ~pstate
+      load_loop ~stack
     with
       End_of_input ->
-      pstate
+      stack
   in
-  let pstate = load_loop ~pstate in
+  let stack = load_loop ~stack in
   (* If Load left a proof open, we fail too. *)
-  if there_are_pending_proofs ~pstate then
+  if there_are_pending_proofs ~stack then
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
-  pstate
+  stack
 
 and interp_control ?proof ~st v = match v with
   | { v=VernacExpr (atts, cmd) } ->
     interp_expr ?proof ~atts ~st cmd
   | { v=VernacFail v } ->
     with_fail ~st (fun () -> interp_control ?proof ~st v);
-    st.Vernacstate.proof
+    st.Vernacstate.lemmas
   | { v=VernacTimeout (timeout,v) } ->
     vernac_timeout ~timeout (interp_control ?proof ~st) v
   | { v=VernacRedirect (s, v) } ->
@@ -2774,8 +2780,8 @@ let interp ?(verbosely=true) ?proof ~st cmd =
   Vernacstate.unfreeze_interp_state st;
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
-      let pstate = v_mod (interp_control ?proof ~st) cmd in
-      Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"];
+      let ontop = v_mod (interp_control ?proof ~st) cmd in
+      Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
   with exn ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index d94ddc1aaf..f1c8b29313 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
 (** The main interpretation function of vernacular expressions *)
 val interp :
   ?verbosely:bool ->
-  ?proof:Proof_global.closed_proof ->
+  ?proof:(Proof_global.proof_object * Lemmas.proof_terminator) ->
   st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
@@ -41,13 +41,6 @@ val command_focus : unit Proof.focus_kind
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
-(** Helper *)
-val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a
-
-val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> 'a) -> 'a
-
-val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> Proof_global.t) -> Proof_global.stack option
-
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
 val test_mode : bool ref
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 6f8a4e8a3c..6a52177dd5 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -55,9 +55,10 @@ type vernac_classification = vernac_type * vernac_when
 
 type typed_vernac =
   | VtDefault of (unit -> unit)
+
   | VtNoProof of (unit -> unit)
-  | VtCloseProof of (pstate:Proof_global.t -> unit)
-  | VtOpenProof of (unit -> Proof_global.t)
+  | VtCloseProof of (lemma:Lemmas.t -> unit)
+  | VtOpenProof of (unit -> Lemmas.t)
   | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
   | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
   | VtReadProof of (pstate:Proof_global.t -> unit)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 60e371a6d9..78b7f21b0d 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -74,8 +74,8 @@ type vernac_classification = vernac_type * vernac_when
 type typed_vernac =
   | VtDefault of (unit -> unit)
   | VtNoProof of (unit -> unit)
-  | VtCloseProof of (pstate:Proof_global.t -> unit)
-  | VtOpenProof of (unit -> Proof_global.t)
+  | VtCloseProof of (lemma:Lemmas.t -> unit)
+  | VtOpenProof of (unit -> Lemmas.t)
   | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
   | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
   | VtReadProof of (pstate:Proof_global.t -> unit)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 0fbde1ade5..90075cbb70 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -30,18 +30,16 @@ end
 type t = {
   parsing : Parser.state;
   system  : States.state;          (* summary + libstack *)
-  proof   : Proof_global.stack option; (* proof state *)
+  lemmas  : Lemmas.Stack.t option; (* proofs of lemmas currently opened *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
-let pstate st = Option.map Proof_global.get_current_pstate st.proof
-
 let s_cache = ref None
-let s_proof = ref None
+let s_lemmas = ref None
 
 let invalidate_cache () =
   s_cache := None;
-  s_proof := None
+  s_lemmas := None
 
 let update_cache rf v =
   rf := Some v; v
@@ -57,14 +55,14 @@ let do_if_not_cached rf f v =
 
 let freeze_interp_state ~marshallable =
   { system = update_cache s_cache (States.freeze ~marshallable);
-    proof  = !s_proof;
+    lemmas = !s_lemmas;
     shallow = false;
     parsing = Parser.cur_state ();
   }
 
-let unfreeze_interp_state { system; proof; parsing } =
+let unfreeze_interp_state { system; lemmas; parsing } =
   do_if_not_cached s_cache States.unfreeze system;
-  s_proof := proof;
+  s_lemmas := lemmas;
   Pcoq.unfreeze parsing
 
 let make_shallow st =
@@ -77,11 +75,16 @@ let make_shallow st =
 (* Compatibility module *)
 module Proof_global = struct
 
-  let get () = !s_proof
-  let set x = s_proof := x
+  type t = Lemmas.Stack.t
+
+  let get () = !s_lemmas
+  let set x = s_lemmas := x
+
+  let get_pstate () =
+    Option.map (Lemmas.Stack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas
 
   let freeze ~marshallable:_ = get ()
-  let unfreeze x = s_proof := Some x
+  let unfreeze x = s_lemmas := Some x
 
   exception NoCurrentProof
 
@@ -92,53 +95,67 @@ module Proof_global = struct
       | _ -> raise CErrors.Unhandled
     end
 
+  open Lemmas
   open Proof_global
 
-  let cc f = match !s_proof with
+  let cc f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> f x
+    | Some x -> Stack.with_top_pstate ~f x
 
-  let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p))
+  let cc_lemma f = match !s_lemmas with
+    | None -> raise NoCurrentProof
+    | Some x -> Stack.with_top ~f x
 
-  let dd f = match !s_proof with
+  let cc_stack f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> s_proof := Some (f x)
+    | Some x -> f x
 
-  let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p)
+  let dd f = match !s_lemmas with
+    | None -> raise NoCurrentProof
+    | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x)
 
-  let there_are_pending_proofs () = !s_proof <> None
-  let get_open_goals () = cc1 get_open_goals
+  let dd_lemma f = match !s_lemmas with
+    | None -> raise NoCurrentProof
+    | Some x -> s_lemmas := Some (Stack.map_top ~f x)
 
-  let set_terminator x = dd1 (set_terminator x)
-  let give_me_the_proof_opt () = Option.map (fun p -> give_me_the_proof (Proof_global.get_current_pstate p)) !s_proof
-  let give_me_the_proof () = cc1 give_me_the_proof
-  let get_current_proof_name () = cc1 get_current_proof_name
+  let there_are_pending_proofs () = !s_lemmas <> None
+  let get_open_goals () = cc get_open_goals
 
-  let simple_with_current_proof f =
-    dd (simple_with_current_proof f)
+  let set_terminator x = dd_lemma (set_terminator x)
+  let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas
+  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 with_current_proof f =
-    let pf, res = cc (with_current_proof f) in
-    s_proof := Some pf; res
+    match !s_lemmas with
+    | None -> raise NoCurrentProof
+    | Some stack ->
+      let pf, res = Stack.with_top_pstate stack ~f:(with_proof f) in
+      let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in
+      s_lemmas := Some stack;
+      res
+
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
 
-  let install_state s = s_proof := Some s
 
-  let return_proof ?allow_partial () =
-    cc1 (return_proof ?allow_partial)
+  let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
 
   let close_future_proof ~opaque ~feedback_id pf =
-    cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+    cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
+                        get_terminator pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate f =
-    cc1 (close_proof ~opaque ~keep_body_ucst_separate f)
+    cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt,
+                        get_terminator pt)
 
-  let discard_all () = s_proof := None
-  let update_global_env () = dd1 update_global_env
+  let discard_all () = s_lemmas := None
+  let update_global_env () = dd (update_global_env)
 
-  let get_current_context () = cc1 Pfedit.get_current_context
+  let get_current_context () = cc Pfedit.get_current_context
 
   let get_all_proof_names () =
-    try cc get_all_proof_names
+    try cc_stack Lemmas.Stack.get_all_proof_names
     with NoCurrentProof -> []
 
   let copy_terminators ~src ~tgt =
@@ -146,6 +163,6 @@ module Proof_global = struct
     | None, None -> None
     | Some _ , None -> None
     | None, Some x -> Some x
-    | Some src, Some tgt -> Some (copy_terminators ~src ~tgt)
+    | Some src, Some tgt -> Some (Stack.copy_terminators ~src ~tgt)
 
 end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b0f3c572e5..1bb18116b5 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -18,14 +18,12 @@ module Parser : sig
 
 end
 
-type t = {
-  parsing : Parser.state;
-  system  : States.state;          (* summary + libstack *)
-  proof   : Proof_global.stack option; (* proof state *)
-  shallow : bool                   (* is the state trimmed down (libstack) *)
-}
-
-val pstate : t -> Proof_global.t option
+type t =
+  { parsing : Parser.state
+  ; system  : States.state          (* summary + libstack *)
+  ; lemmas  : Lemmas.Stack.t option (* proofs of lemmas currently opened *)
+  ; shallow : bool                  (* is the state trimmed down (libstack) *)
+  }
 
 val freeze_interp_state : marshallable:bool -> t
 val unfreeze_interp_state : t -> unit
@@ -38,21 +36,12 @@ val invalidate_cache : unit -> unit
 (* Compatibility module: Do Not Use *)
 module Proof_global : sig
 
-  open Proof_global
-
-  (* Low-level stuff *)
-  val get : unit -> stack option
-  val set : stack option -> unit
-
-  val freeze : marshallable:bool -> stack option
-  val unfreeze : stack -> unit
-
   exception NoCurrentProof
 
   val there_are_pending_proofs : unit -> bool
   val get_open_goals : unit -> int
 
-  val set_terminator : proof_terminator -> unit
+  val set_terminator : Lemmas.proof_terminator -> unit
   val give_me_the_proof : unit -> Proof.t
   val give_me_the_proof_opt : unit -> Proof.t option
   val get_current_proof_name : unit -> Names.Id.t
@@ -63,16 +52,17 @@ module Proof_global : sig
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-  val install_state : stack -> unit
 
-  val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
+  val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
+
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
 
   val close_future_proof :
-    opaque:opacity_flag ->
+    opaque:Proof_global.opacity_flag ->
     feedback_id:Stateid.t ->
-    closed_proof_output Future.computation -> closed_proof
+    Proof_global.closed_proof_output Future.computation -> closed_proof
 
-  val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
+  val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
   val discard_all : unit -> unit
   val update_global_env : unit -> unit
@@ -81,7 +71,19 @@ module Proof_global : sig
 
   val get_all_proof_names : unit -> Names.Id.t list
 
-  val copy_terminators : src:stack option -> tgt:stack option -> stack option
+  val copy_terminators : src:Lemmas.Stack.t option -> tgt:Lemmas.Stack.t option -> Lemmas.Stack.t option
+
+  (* Handling of the imperative state *)
+  type t = Lemmas.Stack.t
+
+  (* Low-level stuff *)
+  val get : unit -> t option
+  val set : t option -> unit
+
+  val get_pstate : unit -> Proof_global.t option
+
+  val freeze : marshallable:bool -> t option
+  val unfreeze : t -> unit
 
 end
 [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]