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.

11 files changed, 198 insertions, 178 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ea66234993..c783531f91 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -309,7 +309,7 @@ let id_of_class cl =
 	  mip.(0).Declarations.mind_typename
     | _ -> assert false
 
-let instance_hook k info global imps ?hook cst =
+let instance_hook info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst imps;
   let info = intern_info info in
   let env = Global.env () in
@@ -317,7 +317,7 @@ let instance_hook k info global imps ?hook cst =
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook id decl poly sigma term termtype =
   (* XXX: Duplication of the declare_constant path *)
   let kind = IsDefinition Instance in
   let sigma =
@@ -331,7 +331,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
   let kn = Declare.declare_constant id cdecl in
   Declare.definition_message id;
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
-  instance_hook k info global imps ?hook (ConstRef kn)
+  instance_hook info global imps ?hook (ConstRef kn)
 
 let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
   let subst = List.fold_left2
@@ -344,66 +344,65 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
       (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook k pri global imps (ConstRef cst)
+  instance_hook pri global imps (ConstRef cst)
 
-let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
+let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
+  let hook _ _ vis gr =
+    let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+    Impargs.declare_manual_implicits false gr imps;
+    let pri = intern_info pri in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    declare_instance env sigma (Some pri) (not global) (ConstRef cst)
+  in
+  let obls, constr, typ =
+    match term with
+    | Some t ->
+      let termtype = EConstr.of_constr termtype in
+      let obls, _, constr, typ =
+        Obligations.eterm_obligations env id sigma 0 t termtype
+      in obls, Some constr, typ
+    | None -> [||], None, termtype
+  in
+  let hook = Lemmas.mk_hook hook in
+  let ctx = Evd.evar_universe_context sigma in
+  ignore(Obligations.add_definition id ?term:constr
+           ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
+
+
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+  (* spiwack: it is hard to reorder the actions to do
+     the pretyping after the proof has opened. As a
+     consequence, we use the low-level primitives to code
+     the refinement manually.*)
+  let gls = List.rev (Evd.future_goals sigma) in
+  let sigma = Evd.reset_future_goals sigma in
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-  if program_mode then
-    let hook _ _ vis gr =
-      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-      Impargs.declare_manual_implicits false gr imps;
-      let pri = intern_info pri in
-      let env = Global.env () in
-      let sigma = Evd.from_env env in
-      declare_instance env sigma (Some pri) (not global) (ConstRef cst)
-    in
-    let obls, constr, typ =
-      match term with
-      | Some t ->
-        let termtype = EConstr.of_constr termtype in
-        let obls, _, constr, typ =
-          Obligations.eterm_obligations env id sigma 0 t termtype
-        in obls, Some constr, typ
-      | None -> [||], None, termtype
-    in
-    let hook = Lemmas.mk_hook hook in
-    let ctx = Evd.evar_universe_context sigma in
-    let _progress = Obligations.add_definition id ?term:constr
-              ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in
+  let pstate = Lemmas.start_proof 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 =
+    if not (Option.is_empty term) then
+      let init_refine =
+        Tacticals.New.tclTHENLIST [
+          Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
+          Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
+          Tactics.New.reduce_after_refine;
+        ]
+      in
+      let pstate, _ = Pfedit.by init_refine pstate in
+      pstate
+    else
+      let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
+      pstate
+  in
+  match tac with
+  | Some tac ->
+    let pstate, _ = Pfedit.by tac pstate in
+    pstate
+  | None ->
     pstate
-  else
-    Some Flags.(silently (fun () ->
-        (* spiwack: it is hard to reorder the actions to do
-           the pretyping after the proof has opened. As a
-           consequence, we use the low-level primitives to code
-           the refinement manually.*)
-        let gls = List.rev (Evd.future_goals sigma) in
-        let sigma = Evd.reset_future_goals sigma in
-        let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype)
-          ~hook:(Lemmas.mk_hook
-             (fun _ _ _ -> instance_hook k pri global imps ?hook)) in
-        (* spiwack: I don't know what to do with the status here. *)
-        let pstate =
-          if not (Option.is_empty term) then
-            let init_refine =
-              Tacticals.New.tclTHENLIST [
-                Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
-                Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
-                Tactics.New.reduce_after_refine;
-              ]
-            in
-            let pstate, _ = Pfedit.by init_refine pstate in
-            pstate
-          else
-            let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
-            pstate
-        in
-        match tac with
-        | Some tac ->
-          let pstate, _ = Pfedit.by tac pstate in
-          pstate
-        | None ->
-          pstate) ())
 
 let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
   let props =
@@ -487,10 +486,18 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct
   let pstate =
     if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
       let term = to_constr sigma (Option.get term) in
-      (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
-       None)
-    else if program_mode || Option.is_empty props then
-      declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
+      (declare_instance_constant pri global imps ?hook id decl poly sigma term termtype;
+       pstate)
+    else if program_mode then
+      (declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype ; pstate)
+    else if Option.is_empty props then
+      let pstate' =
+        Flags.silently (fun () ->
+            declare_instance_open sigma ?hook ~tac ~global ~poly
+              id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
+          ()
+      in
+      Some (Proof_global.push ~ontop:pstate pstate')
     else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
   id, pstate
 
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 8d5f3e3a06..f80dbb9897 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -31,20 +31,6 @@ 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 declare_instance_constant :
-  typeclass ->
-  Hints.hint_info_expr (** priority *) ->
-  bool (** globality *) ->
-  Impargs.manual_explicitation list (** implicits *) ->
-  ?hook:(GlobRef.t -> unit) ->
-  Id.t (** name *) ->
-  UState.universe_decl ->
-  bool (** polymorphic *) ->
-  Evd.evar_map (** Universes *) ->
-  Constr.t (** body *) ->
-  Constr.types (** type *) ->
-  unit
-
 val new_instance :
   pstate:Proof_global.t option
   -> ?global:bool (** Not global by default. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a428c42e49..006ac314a5 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   let pstate =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
@@ -267,7 +267,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
         fixdefs) in
     let evd = Evd.from_ctx ctx in
     Some
-    (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
+    (Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
       evd pl (Some(false,indexes,init_tac)) thms None)
   else begin
     (* We shortcut the proof process *)
@@ -294,7 +294,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   pstate
 
-let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   let pstate =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
@@ -305,7 +305,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
-    Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
+    Some (Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
             evd pl (Some(true,[],init_tac)) thms None)
   else begin
     (* We shortcut the proof process *)
@@ -366,18 +366,18 @@ let check_safe () =
   let flags = Environ.typing_flags (Global.env ()) in
   flags.check_universes && flags.check_guarded
 
-let do_fixpoint ~ontop local poly l =
+let do_fixpoint local poly l =
   let fixl, ntns = extract_fixpoint_components ~structonly:true l in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
   let possible_indexes =
     List.map compute_possible_guardness_evidences info in
-  let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
+  let pstate = declare_fixpoint local poly fix possible_indexes ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   pstate
 
-let do_cofixpoint ~ontop local poly l =
+let do_cofixpoint local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
   let cofix = interp_fixpoint ~cofix:true fixl ntns in
-  let pstate = declare_cofixpoint ~ontop local poly cofix ntns in
+  let pstate = declare_cofixpoint local poly cofix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   pstate
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 5937842f17..d36593332e 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,14 +19,12 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  ontop:Proof_global.t option ->
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.pstate option
 
 val do_cofixpoint :
-  ontop:Proof_global.t option ->
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.pstate option
 
 (************************************************************************)
 (** Internal API  *)
@@ -83,20 +81,18 @@ val interp_fixpoint :
 
 (** [Not used so far] *)
 val declare_fixpoint :
-  ontop:Proof_global.t option ->
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list ->
-  Proof_global.t option
+  Proof_global.pstate option
 
 val declare_cofixpoint :
-  ontop:Proof_global.t option ->
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   decl_notation list ->
-  Proof_global.t option
+  Proof_global.pstate option
 
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 740b9031cc..d0ec575eb3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -329,7 +329,7 @@ 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 ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof 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
@@ -340,7 +340,7 @@ let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?
     | None -> initialize_named_context_for_proof ()
   in
   let goals = [ Global.env_of_context sign , c ] in
-  Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator
+  Proof_global.start_proof sigma id ?pl kind goals terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -356,7 +356,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 ~ontop ?hook kind sigma decl recguard thms snl =
+let start_proof_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) ->
@@ -388,14 +388,14 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
-      let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let pstate = Proof_global.simple_with_current_proof (fun _ p ->
+      let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+      let pstate = Proof_global.modify_proof (fun p ->
           match init_tac with
           | None -> p
           | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
       pstate
 
-let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
+let start_proof_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
@@ -427,7 +427,7 @@ let start_proof_com ~program_mode ~ontop ?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 ~ontop ?hook kind evd decl recguard thms snl
+  start_proof_with_initialization ?hook kind evd decl recguard thms snl
 
 (* Saving a proof *)
 
@@ -487,20 +487,26 @@ let save_proof_admitted ?proof ~pstate =
   in
   Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
 
-let save_proof_proved ?proof ?pstate ~opaque ~idopt =
+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)))
+
+let save_proof_proved ?proof ?ontop ~opaque ~idopt =
   (* Invariant (uh) *)
-  if Option.is_empty pstate && Option.is_empty proof then
+  if Option.is_empty ontop && 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 = Option.get pstate in
+      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
     | Some proof -> proof
   in
   (* if the proof is given explicitly, nothing has to be deleted *)
-  let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in
+  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)));
-  pstate
+  ontop
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1f70cfa1ad..ad6eb024aa 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -37,26 +37,25 @@ val call_hook
   -> ?fix_exn:Future.fix_exn
   -> hook_type
 
-val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
+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
+  ?hook:declaration_hook -> EConstr.types -> Proof_global.pstate
 
 val start_proof_com
   :  program_mode:bool
-  -> ontop:Proof_global.t option
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
-  -> Proof_global.t
+  -> Proof_global.pstate
 
-val start_proof_with_initialization : ontop:Proof_global.t option ->
+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
+  -> int list option -> Proof_global.pstate
 
 val standard_proof_terminator :
   ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
@@ -73,12 +72,18 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 val save_proof_admitted
   :  ?proof:Proof_global.closed_proof
-  -> pstate:Proof_global.t
+  -> pstate:Proof_global.pstate
   -> unit
 
 val save_proof_proved
   :  ?proof:Proof_global.closed_proof
-  -> ?pstate:Proof_global.t
+  -> ?ontop:Proof_global.t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> Proof_global.t option
+
+val save_pstate_proved
+  : pstate:Proof_global.pstate
+  -> opaque:Proof_global.opacity_flag
+  -> idopt:Names.lident option
+  -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bc741a0ec7..0d93e19723 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -760,7 +760,7 @@ let update_obls prg obls rem =
       match prg'.prg_deps with
       | [] ->
           let kn = declare_definition prg' in
-	    progmap_remove prg';
+            progmap_remove prg';
 	    Defined kn
       | l ->
 	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
@@ -944,7 +944,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
       ignore (auto (Some prg.prg_name) None deps)
   end
 
-let rec solve_obligation ~ontop prg num tac =
+let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -965,19 +965,19 @@ let rec solve_obligation ~ontop prg num tac =
     Proof_global.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 ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook 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
 
-and obligation ~ontop (user_num, name, typ) tac =
+and obligation (user_num, name, typ) tac =
   let num = pred user_num in
   let prg = get_prog_err name in
   let obls, rem = prg.prg_obligations in
     if num >= 0 && num < Array.length obls then
       let obl = obls.(num) in
 	match obl.obl_body with
-          | None -> solve_obligation ~ontop prg num tac
+          | None -> solve_obligation prg num tac
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
 
@@ -1177,7 +1177,7 @@ let admit_obligations n =
     let prg = get_prog_err n in
     admit_prog prg
 
-let next_obligation ~ontop n tac =
+let next_obligation n tac =
   let prg = match n with
   | None -> get_any_prog_err ()
   | Some _ -> get_prog_err n
@@ -1188,7 +1188,7 @@ let next_obligation ~ontop n tac =
   | Some i -> i
   | None -> anomaly (Pp.str "Could not find a solvable obligation.")
   in
-  solve_obligation ~ontop prg i tac
+  solve_obligation prg i tac
 
 let check_program_libraries () =
   Coqlib.check_required_library Coqlib.datatypes_module_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 9214ddd4b9..7db094a75d 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -86,16 +86,14 @@ val add_mutual_definitions :
   fixpoint_kind -> unit
 
 val obligation
-  :  ontop:Proof_global.t option
-  -> 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
+  -> Proof_global.pstate
 
 val next_obligation
-  :  ontop:Proof_global.t option
-  -> Names.Id.t option
+  : Names.Id.t option
   -> Genarg.glob_generic_argument option
-  -> Proof_global.t
+  -> Proof_global.pstate
 
 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/search.mli b/vernac/search.mli
index 0f94ddc5b6..f8074a67ff 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -39,13 +39,13 @@ val search_about_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_about   : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
+val search_about   : ?pstate:Proof_global.pstate -> int option -> (bool * glob_search_about_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
@@ -66,12 +66,12 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Proof_global.pstate -> ?glnum:int -> (search_constraint * bool) list ->
   constr coq_object list
 
 (** {6 Generic search function} *)
 
-val generic_search : ?pstate:Proof_global.t -> int option -> display_function -> unit
+val generic_search : ?pstate:Proof_global.pstate -> int option -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 337cb233a2..f92c1f9c27 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -56,6 +56,10 @@ let vernac_require_open_proof ~pstate f =
   | Some pstate -> f ~pstate
   | 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 get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
@@ -540,7 +544,7 @@ let () =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print ~program_mode ~pstate ?hook k l =
+let start_proof_and_print ~program_mode ?hook k l =
   let inference_hook =
     if program_mode then
       let hook env sigma ev =
@@ -562,7 +566,7 @@ let start_proof_and_print ~program_mode ~pstate ?hook k l =
       in Some hook
     else None
   in
-  start_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l
+  start_proof_com ~program_mode ?inference_hook ?hook k l
 
 let vernac_definition_hook p = function
 | Coercion ->
@@ -573,7 +577,7 @@ let vernac_definition_hook p = function
   Some (Class.add_subclass_hook p)
 | _ -> None
 
-let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
+let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def ~pstate =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
@@ -593,9 +597,10 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
-      Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind)
+      Some (start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind)
               ?hook [(CAst.make ?loc name, pl), (bl, t)])
     | DefineBody (bl,red_option,c,typ_opt) ->
+      let pstate = Option.map Proof_global.get_current_pstate pstate in
       let red_option = match red_option with
         | None -> None
         | Some r ->
@@ -603,30 +608,31 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
           Some (snd (Hook.get f_interp_redexp env sigma r)) in
       ComDefinition.do_definition ~program_mode name
         (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
-      pstate
+      None
   )
 
-let vernac_start_proof ~atts ~pstate kind l =
+(* NB: pstate argument to use combinators easily *)
+let vernac_start_proof ~atts kind l ~pstate =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
+  Some (start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
 
-let vernac_end_proof ?pstate ?proof = function
+let vernac_end_proof ?pstate:ontop ?proof = function
   | Admitted ->
-    vernac_require_open_proof ~pstate (save_proof_admitted ?proof);
-    pstate
+    with_pstate ~pstate:ontop (save_proof_admitted ?proof);
+    ontop
   | Proved (opaque,idopt) ->
-    save_proof_proved ?pstate ?proof ~opaque ~idopt
+    save_proof_proved ?ontop ?proof ~opaque ~idopt
 
-let vernac_exact_proof ~pstate c =
+let vernac_exact_proof ~pstate:ontop 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 pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
+  let pstate, status = Pfedit.by (Tactics.exact_proof c) (Proof_global.get_current_pstate ontop) in
+  let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom;
-  pstate
+  Proof_global.discard_current ontop
 
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
@@ -804,7 +810,7 @@ let vernac_inductive ~atts cum lo finite indl =
       in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
     *)
 
-let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
+let vernac_fixpoint ~atts discharge l ~pstate =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
@@ -813,11 +819,11 @@ let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
   let do_fixpoint = if atts.program then
       fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None
     else
-      ComFixpoint.do_fixpoint ~ontop:pstate
+      ComFixpoint.do_fixpoint
   in
   do_fixpoint local atts.polymorphic l
 
-let vernac_cofixpoint ~atts ~pstate discharge l =
+let vernac_cofixpoint ~atts discharge l ~pstate =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
@@ -825,7 +831,7 @@ let vernac_cofixpoint ~atts ~pstate discharge l =
   let do_cofixpoint = if atts.program then
       fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None
     else
-      ComFixpoint.do_cofixpoint ~ontop:pstate
+      ComFixpoint.do_cofixpoint
   in
   do_cofixpoint local atts.polymorphic l
 
@@ -1104,7 +1110,7 @@ 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 : Proof_global.pstate) e : Proof_global.pstate =
   let env = Global.env () in
   let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
   let tys =
@@ -1118,9 +1124,7 @@ let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
         (str "Unknown variable: " ++ Id.print id))
     l;
   let _, pstate = Proof_global.set_used_variables pstate l in
-  fst @@ Proof_global.with_current_proof begin fun _ p ->
-    (p, ())
-  end pstate
+  pstate
 
 (*****************************)
 (* Auxiliary file management *)
@@ -1829,6 +1833,7 @@ let query_command_selector ?loc = function
       (str "Query commands only support the single numbered goal selector.")
 
 let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
+  let pstate = Option.map Proof_global.get_current_pstate pstate in
   let glopt = query_command_selector glopt in
   let sigma, env = get_current_context_of_args ~pstate glopt in
   let sigma, c = interp_open_constr env sigma rc in
@@ -1929,6 +1934,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     print_about env sigma ref_or_by_not udecl
 
 let vernac_print ~(pstate : Proof_global.t option) ~atts =
+  let pstate = Option.map Proof_global.get_current_pstate pstate in
   let sigma, env = get_current_or_global_context ~pstate in
   function
   | PrintTables -> print_tables ()
@@ -2040,6 +2046,7 @@ let () =
       optwrite = (:=) search_output_name_only }
 
 let vernac_search ~pstate ~atts s gopt r =
+  let pstate = Option.map Proof_global.get_current_pstate pstate in
   let gopt = query_command_selector gopt in
   let r = interp_search_restriction r in
   let env,gopt =
@@ -2077,6 +2084,7 @@ let vernac_locate ~pstate = function
   | LocateTerm {v=AN qid} -> print_located_term qid
   | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
   | LocateTerm {v=ByNotation (ntn, sc)} ->
+    let pstate = Option.map Proof_global.get_current_pstate pstate in
     let _, env = get_current_or_global_context ~pstate in
     Notation.locate_notation
       (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
@@ -2132,6 +2140,7 @@ let vernac_unfocus () =
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused ~pstate =
+  let pstate = Proof_global.get_current_pstate pstate in
   let p = Proof_global.give_me_the_proof pstate in
   if Proof.unfocused p then
     str"The proof is indeed fully unfocused."
@@ -2162,18 +2171,19 @@ let vernac_bullet (bullet : Proof_bullet.t) =
   Proof_global.simple_with_current_proof (fun _ p ->
     Proof_bullet.put p bullet)
 
-let vernac_show ~pstate =
-  match pstate with
+let vernac_show ~pstate:ontop =
+  match ontop with
   (* Show functions that don't require a proof state *)
   | None ->
     begin function
-      | ShowProof -> show_proof ~pstate
+      | ShowProof -> show_proof ~pstate:None
       | ShowMatch id -> show_match id
       | _ ->
         user_err (str "This command requires an open proof.")
     end
   (* Show functions that require a proof state *)
-  | Some pstate ->
+  | Some ontop ->
+    let pstate = Proof_global.get_current_pstate ontop in
     begin function
     | ShowGoal goalref ->
       let proof = Proof_global.give_me_the_proof pstate in
@@ -2185,7 +2195,7 @@ let vernac_show ~pstate =
     | ShowExistentials -> show_top_evars ~pstate
     | ShowUniverses -> show_universes ~pstate
     | ShowProofNames ->
-      pr_sequence Id.print (Proof_global.get_all_proof_names pstate)
+      pr_sequence Id.print (Proof_global.get_all_proof_names ontop)
     | ShowIntros all -> show_intro ~pstate all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
@@ -2223,6 +2233,10 @@ let with_def_attributes ~atts f =
   if atts.DefAttributes.program then Obligations.check_program_libraries ();
   f ~atts
 
+let with_maybe_open_proof ~pstate f =
+  let opt = f ~pstate in
+  Proof_global.maybe_push ~ontop:pstate opt
+
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
@@ -2339,9 +2353,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
 
   (* Gallina *)
   | VernacDefinition ((discharge,kind),lid,d) ->
-    with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d
+    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_definition discharge kind lid d)
   | VernacStartTheoremProof (k,l) ->
-    with_def_attributes ~atts vernac_start_proof ~pstate k l
+    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_start_proof k l)
   | VernacEndProof e ->
     unsupported_attributes atts;
     vernac_end_proof ?proof ?pstate e
@@ -2355,9 +2369,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     vernac_inductive ~atts cum priv finite l;
     pstate
   | VernacFixpoint (discharge, l) ->
-    with_def_attributes ~atts vernac_fixpoint ~pstate discharge l
+    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_fixpoint discharge l)
   | VernacCoFixpoint (discharge, l) ->
-    with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l
+    with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_cofixpoint discharge l)
   | VernacScheme l ->
     unsupported_attributes atts;
     vernac_scheme l;
@@ -2587,7 +2601,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
   | VernacCheckGuard ->
     unsupported_attributes atts;
     Feedback.msg_notice @@
-      vernac_require_open_proof ~pstate (vernac_check_guard);
+      with_pstate ~pstate (vernac_check_guard);
     pstate
   | VernacProof (tac, using) ->
     unsupported_attributes atts;
@@ -2596,10 +2610,14 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     let usings = if Option.is_empty using then "using:no" else "using:yes" in
     Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
     let pstate =
-      vernac_require_open_proof ~pstate (fun ~pstate ->
+      vernac_require_open_proof ~pstate (fun ~pstate:ontop ->
+          Proof_global.modify_current_pstate (fun pstate ->
+          let pstate = Proof_global.get_current_pstate ontop in
           let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
           Option.cata (vernac_set_used_variables ~pstate) pstate using)
-    in Some pstate
+            ontop)
+    in
+    Some pstate
   | VernacProofMode mn ->
     unsupported_attributes atts;
     pstate
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 77f54361da..9ab2d00fc2 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -96,17 +96,21 @@ module Proof_global = struct
     | None -> raise NoCurrentProof
     | Some x -> f x
 
+  let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p))
+
   let dd f = match !s_proof with
     | None -> raise NoCurrentProof
     | Some x -> s_proof := Some (f x)
 
+  let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p)
+
   let there_are_pending_proofs () = !s_proof <> None
-  let get_open_goals () = cc get_open_goals
+  let get_open_goals () = cc1 get_open_goals
 
-  let set_terminator x = dd (set_terminator x)
-  let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof
-  let give_me_the_proof () = cc give_me_the_proof
-  let get_current_proof_name () = cc get_current_proof_name
+  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 simple_with_current_proof f =
     dd (simple_with_current_proof f)
@@ -118,18 +122,18 @@ module Proof_global = struct
   let install_state s = s_proof := Some s
 
   let return_proof ?allow_partial () =
-    cc (return_proof ?allow_partial)
+    cc1 (return_proof ?allow_partial)
 
   let close_future_proof ~opaque ~feedback_id pf =
-    cc (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+    cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf)
 
   let close_proof ~opaque ~keep_body_ucst_separate f =
-    cc (close_proof ~opaque ~keep_body_ucst_separate f)
+    cc1 (close_proof ~opaque ~keep_body_ucst_separate f)
 
   let discard_all () = s_proof := None
-  let update_global_env () = dd update_global_env
+  let update_global_env () = dd1 update_global_env
 
-  let get_current_context () = cc Pfedit.get_current_context
+  let get_current_context () = cc1 Pfedit.get_current_context
 
   let get_all_proof_names () =
     try cc get_all_proof_names