[proof_global] Removal of imperative state.

We change the API; after some thinking the tradeoff is clear in favor
of the more radical functional option from the start.

We also guarante the existence of a proof is by typing now,
so exceptions `NoCurrentProof` and `NoSuchGoal` are gone.

TODO: Review what's going on with focusing now.

4 files changed, 163 insertions, 231 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9509c36ec0..472db790f2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -37,41 +37,35 @@ let get_nth_V82_goal p i =
   try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
-let get_goal_context_gen p i =
-  let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in
+let get_goal_context_gen pf i =
+  let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
-let get_goal_context i =
-  try get_goal_context_gen (Proof_global.give_me_the_proof ()) i
-  with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
-     | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
-
-let get_current_goal_context () =
-  try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1
-  with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
-     | NoSuchGoal -> 
-    (* spiwack: returning empty evar_map, since if there is no goal, under focus,
-        there is no accessible evar either *)
-    let env = Global.env () in
-    (Evd.from_env env, env)
+let get_goal_context pf i =
+  let p = Proof_global.give_me_the_proof pf in
+  get_goal_context_gen p i
 
-let get_current_context ?p () =
-  let current_proof_by_default = function
-    | Some p -> p
-    | None -> Proof_global.give_me_the_proof ()
-  in
-  try get_goal_context_gen (current_proof_by_default p) 1
-  with Proof_global.NoCurrentProof ->
+let get_current_goal_context pf =
+  let p = Proof_global.give_me_the_proof pf in
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal ->
+    (* spiwack: returning empty evar_map, since if there is no goal,
+       under focus, there is no accessible evar either. EJGA: this
+       seems strange, as we have pf *)
     let env = Global.env () in
-    (Evd.from_env env, env)
-     | NoSuchGoal ->
-        (* No more focused goals ? *)
-        let p = (current_proof_by_default p) in
-        let evd = Proof.in_proof p (fun x -> x) in
-        (evd, Global.env ())
+    Evd.from_env env, env
+
+let get_current_context pf =
+  let p = Proof_global.give_me_the_proof pf in
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal ->
+    (* No more focused goals *)
+    let evd = Proof.in_proof p (fun x -> x) in
+    evd, Global.env ()
 
 let solve ?with_end_tac gi info_lvl tac pr =
-  try 
     let tac = match with_end_tac with
       | None -> tac
       | Some etac -> Proofview.tclTHEN tac etac in
@@ -112,15 +106,12 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
     in
     (p,status)
-  with
-    Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
-let instantiate_nth_evar_com n com = 
+let instantiate_nth_evar_com n com =
   Proof_global.simple_with_current_proof (fun _ p ->
-      Proof.V82.instantiate_evar Global.(env ())n com p)
-
+      Proof.V82.instantiate_evar Global.(env ()) n com p)
 
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
@@ -133,21 +124,19 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  Proof_global.start_proof evd id goal_kind goals terminator;
+  let pf = Proof_global.start_proof ~ontop:None evd id goal_kind goals terminator in
   try
-    let status = by tac in
+    let pf, status = by tac pf in
     let open Proof_global in
-    let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in
+    let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
     match entries with
     | [entry] ->
-      discard_current ();
       let univs = UState.demote_seff_univs entry universes in
       entry, status, univs
     | _ ->
       CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
   with reraise ->
     let reraise = CErrors.push reraise in
-    Proof_global.discard_current ();
     iraise reraise
 
 let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 29ab00876a..2fe4bc6385 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -16,29 +16,29 @@ open Environ
 open Decl_kinds
 
 (** {6 ... } *)
+
+exception NoSuchGoal
+
 (** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
-val get_goal_context : int -> Evd.evar_map * env
+val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
 
 (** [get_current_goal_context ()] works as [get_goal_context 1] *)
-
-val get_current_goal_context : unit -> Evd.evar_map * env
+val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
 
 (** [get_current_context ()] returns the context of the
   current focused goal. If there is no focused goal but there
   is a proof in progress, it returns the corresponding evar_map.
   If there is no pending proof then it returns the current global
   environment and empty evar_map. *)
-
-val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
+val get_current_context : Proof_global.t -> Evd.evar_map * env
 
 (** {6 ... } *)
 
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
-    subgoal of the current focused proof or raises a [UserError] if no
-    proof is focused or if there is no [n]th subgoal. [solve SelectAll
+    subgoal of the current focused proof. [solve SelectAll
     tac] applies [tac] to all subgoals. *)
 
 val solve : ?with_end_tac:unit Proofview.tactic ->
@@ -46,11 +46,10 @@ val solve : ?with_end_tac:unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
-    focused proof or raises a UserError if there is no focused proof or
-    if there is no more subgoals.
+    focused proof.
     Returns [false] if an unsafe tactic has been used. *)
 
-val by : unit Proofview.tactic -> bool
+val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
 
 (** Option telling if unification heuristics should be used. *)
 val use_unification_heuristics : unit -> bool
@@ -60,7 +59,7 @@ val use_unification_heuristics : unit -> bool
    UserError if no proof is focused or if there is no such [n]th
    existential variable *)
 
-val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
+val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> Proof_global.t -> Proof_global.t
 
 (** [build_by_tactic typ tac] returns a term of type [typ] by calling
     [tac]. The return boolean, if [false] indicates the use of an unsafe
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 6174b75a96..0fefb215e2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -17,7 +17,6 @@
 (***********************************************************************)
 
 open Util
-open Pp
 open Names
 open Context
 
@@ -55,108 +54,66 @@ type pstate = {
   strength : Decl_kinds.goal_kind;
 }
 
-type t = pstate list
+(* The head of [t] is the actual current proof, the other ones are
+   to be resumed when the current proof is closed or aborted. *)
+type t = pstate * pstate list
+
+let pstate_map f (pf, pfl) = (f pf, List.map f pfl)
 
 let make_terminator f = f
 let apply_terminator f = f
 
-(* The head of [!pstates] is the actual current proof, the other ones are
-   to be resumed when the current proof is closed or aborted. *)
-let pstates = ref ([] : pstate list)
-
 (* combinators for the current_proof lists *)
-let push a l = l := a::!l
-
-exception NoCurrentProof
-let () = CErrors.register_handler begin function
-  | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
-  | _ -> raise CErrors.Unhandled
-end
+let push ~ontop a =
+  match ontop with
+  | None -> a , []
+  | Some (l,ls) -> a, (l :: ls)
 
 (*** Proof Global manipulation ***)
 
-let get_all_proof_names () =
-  List.map Proof.(function pf -> (data pf.proof).name) !pstates
-
-let cur_pstate () =
-  match !pstates with
-  | np::_ -> np
-  | [] -> raise NoCurrentProof
-
-let give_me_the_proof () = (cur_pstate ()).proof
-let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
-let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name
-let get_current_persistence () = (cur_pstate ()).strength
-
-let with_current_proof f =
-  match !pstates with
-  | [] -> raise NoCurrentProof
-  | p :: rest ->
-      let et =
-        match p.endline_tactic with
-        | None -> Proofview.tclUNIT ()
-        | Some tac ->
-          let open Geninterp in
-          let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in
-          let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
-          let tac = Geninterp.interp tag ist tac in
-          Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
-      in
-      let (newpr,ret) = f et p.proof in
-      let p = { p with proof = newpr } in
-      pstates := p :: rest;
-      ret
-
-let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
-
-let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
+let get_all_proof_names (pf : t) =
+  let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in
+  pn :: pns
+
+let give_me_the_proof (ps,_) = ps.proof
+let get_current_proof_name (ps,_) = (Proof.data ps.proof).Proof.name
+let get_current_persistence (ps,_) = ps.strength
+
+let with_current_proof f (ps, psl) =
+  let et =
+    match ps.endline_tactic with
+    | None -> Proofview.tclUNIT ()
+    | Some tac ->
+      let open Geninterp in
+      let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in
+      let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
+      let tac = Geninterp.interp tag ist tac in
+      Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
+  in
+  let (newpr,ret) = f et ps.proof in
+  let ps = { ps with proof = newpr } in
+  (ps, psl), ret
+
+let simple_with_current_proof f pf =
+  let p, () = with_current_proof (fun t p -> f t p , ()) pf in p
+
+let compact_the_proof pf = simple_with_current_proof (fun _ -> Proof.compact) pf
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac =
-  match !pstates with
-  | [] -> raise NoCurrentProof
-  | p :: rest -> pstates := { p with endline_tactic = Some tac } :: rest
-
-(* spiwack: it might be considered to move error messages away.
-    Or else to remove special exceptions from Proof_global.
-    Arguments for the former: there is no reason Proof_global is only
-    accessed directly through vernacular commands. Error message should be
-   pushed to external layers, and so we should be able to have a finer
-   control on error message on complex actions. *)
-let msg_proofs () =
-  match get_all_proof_names () with
-    | [] -> (spc () ++ str"(No proof-editing in progress).")
-    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (pr_sequence Id.print l) ++ str".")
-
-let there_is_a_proof () = not (List.is_empty !pstates)
-let there_are_pending_proofs () = there_is_a_proof ()
-let check_no_pending_proof () =
-  if not (there_are_pending_proofs ()) then
-    ()
-  else begin
-    CErrors.user_err
-      (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
-       str"Use \"Abort All\" first or complete proof(s).")
-  end
+let set_endline_tactic tac (ps, psl) =
+  { ps with endline_tactic = Some tac }, psl
 
 let pf_name_eq id ps =
   let Proof.{ name } = Proof.data ps.proof in
   Id.equal name id
 
-let discard_gen id =
-  pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates
-
-let discard {CAst.loc;v=id} =
-  let n = List.length !pstates in
-  discard_gen id;
-  if Int.equal (List.length !pstates) n then
-    CErrors.user_err ?loc
-      ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
+let discard {CAst.loc;v=id} (ps, psl) =
+  match List.filter (fun pf -> not (pf_name_eq id pf)) (ps :: psl) with
+  | [] -> None
+  | ps :: psl -> Some (ps, psl)
 
-let discard_current () =
-  if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
-let discard_all () = pstates := []
+let discard_current (ps, psl) =
+  if List.is_empty psl then None else Some List.(hd psl, tl psl)
 
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
@@ -166,30 +123,30 @@ let discard_all () = pstates := []
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
+let start_proof ~ontop sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
   let initial_state = {
     terminator = CEphemeron.create terminator;
     proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
-    strength = kind;
-    universe_decl = pl } in
-  push initial_state pstates
+    universe_decl = pl;
+    strength = kind } in
+  push ~ontop initial_state
 
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
+let start_dependent_proof ~ontop name ?(pl=UState.default_univ_decl) kind goals terminator =
   let initial_state = {
     terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
-    strength = kind;
-    universe_decl = pl } in
-  push initial_state pstates
+    universe_decl = pl;
+    strength = kind } in
+  push ~ontop initial_state
 
-let get_used_variables () = (cur_pstate ()).section_vars
-let get_universe_decl () = (cur_pstate ()).universe_decl
+let get_used_variables (pf,_) = pf.section_vars
+let get_universe_decl (pf,_) = pf.universe_decl
 
-let set_used_variables l =
+let set_used_variables (ps,psl) l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
@@ -210,20 +167,17 @@ let set_used_variables l =
        else (ctx, all_safe) in
   let ctx, _ =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
-  match !pstates with
-  | [] -> raise NoCurrentProof
-  | p :: rest ->
-      if not (Option.is_empty p.section_vars) then
-        CErrors.user_err Pp.(str "Used section variables can be declared only once");
-      pstates := { p with section_vars = Some ctx} :: rest;
-      ctx, []
-
-let get_open_goals () =
-  let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).proof in
+  if not (Option.is_empty ps.section_vars) then
+    CErrors.user_err Pp.(str "Used section variables can be declared only once");
+  (* EJGA: This is always empty thus we should modify the type *)
+  (ctx, []), ({ ps with section_vars = Some ctx}, psl)
+
+let get_open_goals (ps, _) =
+  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
   List.length goals +
-    List.fold_left (+) 0
+  List.fold_left (+) 0
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
-    List.length shelf
+  List.length shelf
 
 type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
@@ -240,8 +194,8 @@ let private_poly_univs =
   fun () -> !b
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
-                (fpl : closed_proof_output Future.computation) =
-  let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in
+                (fpl : closed_proof_output Future.computation) ps =
+  let { section_vars; proof; terminator; universe_decl; strength } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -339,8 +293,8 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
-let return_proof ?(allow_partial=false) () =
- let { proof } = cur_pstate () in
+let return_proof ?(allow_partial=false) (ps,_) =
+ let { proof } = ps in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
   let Proof.{sigma=evd} = Proof.data proof in
@@ -368,43 +322,44 @@ let return_proof ?(allow_partial=false) () =
     List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
-let close_future_proof ~opaque ~feedback_id proof =
-  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn =
+let close_future_proof ~opaque ~feedback_id (ps, psl) proof =
+  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
+
+let close_proof ~opaque ~keep_body_ucst_separate fix_exn (ps, psl) =
   close_proof ~opaque ~keep_body_ucst_separate ~now:true
-    (Future.from_val ~fix_exn (return_proof ()))
+    (Future.from_val ~fix_exn (return_proof (ps,psl))) ps
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator
-let set_terminator hook =
-  match !pstates with
-  | [] -> raise NoCurrentProof
-  | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
-
-let freeze ~marshallable =
-  if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
-  else !pstates
-let unfreeze s = pstates := s
-let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
+let get_terminator (ps, _) = CEphemeron.get ps.terminator
+let set_terminator hook (ps, psl) =
+  { ps with terminator = CEphemeron.create hook }, psl
+
 let copy_terminators ~src ~tgt =
-  assert(List.length src = List.length tgt);
-  List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
+  let (ps, psl), (ts,tsl) = src, tgt in
+  assert(List.length psl = List.length tsl);
+  {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
 
-let update_global_env pf_info =
+let update_global_env (pf : t) =
+  let res, () =
   with_current_proof (fun _ p ->
      Proof.in_proof p (fun sigma ->
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
        let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
-         (p, ())))
-
-(* XXX: Bullet hook, should be really moved elsewhere *)
-let () =
-  let hook n =
-    try
-      let prf = give_me_the_proof () in
-      (Proof_bullet.suggest prf)
-    with NoCurrentProof -> mt ()
-  in
-  Proofview.set_nosuchgoals_hook hook
+         (p, ()))) pf
+  in res
+
+(* XXX: This hook is used to provide a better error w.r.t. bullets,
+   however the proof engine [surprise!] knows nothing about bullets so
+   here we have a layering violation. The right fix is to modify the
+   entry point to handle this and reraise the exception with the
+   needed information. *)
+(* let _ =
+ *   let hook n =
+ *     try
+ *       let prf = give_me_the_proof pf in
+ *       (Proof_bullet.suggest prf)
+ *     with NoCurrentProof -> mt ()
+ *   in
+ *   Proofview.set_nosuchgoals_hook hook *)
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 38e234eaee..e2e457483b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,23 +13,15 @@
      environment. *)
 
 type t
-val there_are_pending_proofs : unit -> bool
-val check_no_pending_proof : unit -> unit
+val get_current_proof_name : t -> Names.Id.t
+val get_current_persistence : t -> Decl_kinds.goal_kind
+val get_all_proof_names : t -> Names.Id.t list
 
-val get_current_proof_name : unit -> Names.Id.t
-val get_current_persistence : unit -> Decl_kinds.goal_kind
-val get_all_proof_names : unit -> Names.Id.t list
+val discard : Names.lident -> t -> t option
+val discard_current : t -> t option
 
-val discard : Names.lident -> unit
-val discard_current : unit -> unit
-val discard_all : unit -> unit
-
-val give_me_the_proof_opt : unit -> Proof.t option
-exception NoCurrentProof
-val give_me_the_proof : unit -> Proof.t
-(** @raise NoCurrentProof when outside proof mode. *)
-
-val compact_the_proof : unit -> unit
+val give_me_the_proof : t -> Proof.t
+val compact_the_proof : t -> t
 
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
@@ -60,7 +52,7 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
-(** [start_proof id str pl goals terminator] starts a proof of name
+(** [start_proof ~ontop id str pl goals terminator] starts a proof of name
    [id] with goals [goals] (a list of pairs of environment and
    conclusion); [str] describes what kind of theorem/definition this
    is; [terminator] is used at the end of the proof to close the proof
@@ -68,25 +60,25 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
    morphism). The proof is started in the evar map [sigma] (which can
    typically contain universe constraints), and with universe bindings
    pl. *)
-val start_proof :
+val start_proof : ontop:t option ->
   Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
-    proof_terminator -> unit
+    proof_terminator -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
-val start_dependent_proof :
+val start_dependent_proof : ontop:t option ->
   Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
-  Proofview.telescope -> proof_terminator -> unit
+  Proofview.telescope -> proof_terminator -> t
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
   there_are_pending_proofs. *)
-val update_global_env : unit -> unit
+val update_global_env : t -> t
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -96,39 +88,36 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
-val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t ->
+val return_proof : ?allow_partial:bool -> t -> closed_proof_output
+val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
   closed_proof_output Future.computation -> closed_proof
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-val get_terminator : unit -> proof_terminator
-val set_terminator : proof_terminator -> unit
-
-val get_open_goals : unit -> int
+val get_terminator : t -> proof_terminator
+val set_terminator : proof_terminator -> t -> t
+val get_open_goals : t -> int
 
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
+  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
 val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
+  (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Genarg.glob_generic_argument -> unit
+val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 
 (** Sets the section variables assumed by the proof, returns its closure
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
-val set_used_variables :
-  Names.Id.t list -> Constr.named_context * Names.lident list
-val get_used_variables : unit -> Constr.named_context option
+val set_used_variables : t ->
+  Names.Id.t list -> (Constr.named_context * Names.lident list) * t
+
+val get_used_variables : t -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> UState.universe_decl
+val get_universe_decl : t -> UState.universe_decl
 
-val freeze : marshallable:bool -> t
-val unfreeze : t -> unit
-val proof_of_state : t -> Proof.t
 val copy_terminators : src:t -> tgt:t -> t