Merge PR #10674: [declare] Move proof_entry type to declare, put interactive proof data on top of declare.

Reviewed-by: ppedrot

10 files changed, 730 insertions, 28 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 09d7e0278a..edeb27ab88 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -69,7 +69,7 @@ let rec shrink ctx sign c t accu =
 | _ -> assert false
 
 let shrink_entry sign const =
-  let open Proof_global in
+  let open Declare in
   let typ = match const.proof_entry_type with
   | None -> assert false
   | Some t -> t
@@ -151,7 +151,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
+  let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in
   let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
@@ -160,20 +160,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
-  let inst = match const.Proof_global.proof_entry_universes with
+  let inst = match const.Declare.proof_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
     (* We mimic what the kernel does, that is ensuring that no additional
        constraints appear in the body of polymorphic constants. Ideally this
        should be enforced statically. *)
-    let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in
+    let (_, body_uctx), _ = Future.force const.Declare.proof_entry_body in
     let () = assert (Univ.ContextSet.is_empty body_uctx) in
     EInstance.make (Univ.UContext.instance ctx)
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let effs = Evd.concat_side_effects eff
-    Proof_global.(snd (Future.force const.proof_entry_body)) in
+      (snd (Future.force const.Declare.proof_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index e278729f89..96ddbea7b2 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P
    save path *)
 val shrink_entry
   :  ('a, 'b) Context.Named.Declaration.pt list
-  -> 'c Proof_global.proof_entry
-  -> 'c Proof_global.proof_entry * Constr.t list
+  -> 'c Declare.proof_entry
+  -> 'c Declare.proof_entry * Constr.t list
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c23ee4a76e..3a02e5451a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -55,8 +55,20 @@ type constant_obj = {
   cst_locl : import_status;
 }
 
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  proof_entry_feedback : Stateid.t option;
+  proof_entry_type        : Constr.types option;
+  proof_entry_universes   : Entries.universes_entry;
+  proof_entry_opaque      : bool;
+  proof_entry_inline_code : bool;
+}
+
 type 'a constant_entry =
-  | DefinitionEntry of 'a Proof_global.proof_entry
+  | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
@@ -174,7 +186,6 @@ let record_aux env s_ty s_bo =
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
-  let open Proof_global in
   { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     proof_entry_secctx = None;
     proof_entry_type = types;
@@ -184,7 +195,6 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     proof_entry_inline_code = inline}
 
 let cast_proof_entry e =
-  let open Proof_global in
   let (body, ctx), () = Future.force e.proof_entry_body in
   let univs =
     if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
@@ -205,7 +215,6 @@ let cast_proof_entry e =
   }
 
 let cast_opaque_proof_entry e =
-  let open Proof_global in
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -249,7 +258,6 @@ let is_unsafe_typing_flags () =
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 let define_constant ~side_effect ~name cd =
-  let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let in_section = Lib.sections_are_opened () in
   let export, decl, unsafe = match cd with
@@ -299,7 +307,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
-  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
+  | SectionLocalDef of Evd.side_effects proof_entry
   | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 (* This object is only for things which iterate over objects to find
@@ -321,7 +329,6 @@ let declare_variable ~name ~kind d =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let open Proof_global in
       let (body, eff) = Future.force de.proof_entry_body in
       let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
       let eff = get_roles export eff in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 4ae9f6c7ae..4cb876cecb 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -19,14 +19,27 @@ open Entries
    reset works properly --- and will fill some global tables such as
    [Nametab] and [Impargs]. *)
 
+(** Proof entries *)
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  proof_entry_feedback : Stateid.t option;
+  proof_entry_type        : Constr.types option;
+  proof_entry_universes   : Entries.universes_entry;
+  proof_entry_opaque      : bool;
+  proof_entry_inline_code : bool;
+}
+
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type variable_declaration =
-  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
+  | SectionLocalDef of Evd.side_effects proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 type 'a constant_entry =
-  | DefinitionEntry of 'a Proof_global.proof_entry
+  | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
@@ -43,7 +56,7 @@ val declare_variable
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?univs:Entries.universes_entry ->
-  ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
+  ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e2ef05461b..54393dce00 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,17 +124,7 @@ let define internal role id c poly univs =
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = {
-    Proof_global.proof_entry_body =
-      Future.from_val ((c,Univ.ContextSet.empty),
-                       Evd.empty_side_effects);
-    proof_entry_secctx = None;
-    proof_entry_type = None;
-    proof_entry_universes = univs;
-    proof_entry_opaque = false;
-    proof_entry_inline_code = false;
-    proof_entry_feedback = None;
-  } in
+  let entry = Declare.definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
   let () = match internal with
     | InternalTacticRequest -> ()
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
new file mode 100644
index 0000000000..5be7b4fa28
--- /dev/null
+++ b/tactics/pfedit.ml
@@ -0,0 +1,195 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Environ
+open Evd
+
+let use_unification_heuristics_ref = ref true
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname = "Solve unification constraints at every \".\"";
+  optkey = ["Solve";"Unification";"Constraints"];
+  optread = (fun () -> !use_unification_heuristics_ref);
+  optwrite = (fun a -> use_unification_heuristics_ref:=a);
+})
+
+let use_unification_heuristics () = !use_unification_heuristics_ref
+
+exception NoSuchGoal
+let () = CErrors.register_handler begin function
+  | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
+  | _ -> raise CErrors.Unhandled
+end
+
+let get_nth_V82_goal p i =
+  let Proof.{ sigma; goals } = Proof.data p in
+  try { it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise NoSuchGoal
+
+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 pf i =
+  let p = Proof_global.get_proof pf in
+  get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = Proof_global.get_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
+
+let get_current_context pf =
+  let p = Proof_global.get_proof pf in
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal ->
+    (* No more focused goals *)
+    let { Proof.sigma } = Proof.data p in
+    sigma, Global.env ()
+
+let solve ?with_end_tac gi info_lvl tac pr =
+    let tac = match with_end_tac with
+      | None -> tac
+      | Some etac -> Proofview.tclTHEN tac etac in
+    let tac = match info_lvl with
+      | None -> tac
+      | Some _ -> Proofview.Trace.record_info_trace tac
+    in
+    let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in
+    let tac = let open Goal_select in match gi with
+      | SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
+      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
+      | SelectAll -> tac
+    in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
+    in
+    let env = Global.env () in
+    let (p,(status,info),()) = Proof.run_tactic env tac pr in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let () =
+      match info_lvl with
+      | None -> ()
+      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
+    in
+    (p,status)
+
+let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac)
+
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let build_constant_by_tactic ~name ctx sign ~poly typ tac =
+  let evd = Evd.from_ctx ctx in
+  let goals = [ (Global.env_of_context sign , typ) ] in
+  let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
+  try
+    let pf, status = by tac pf in
+    let open Proof_global in
+    let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
+    match entries with
+    | [entry] ->
+      let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes 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
+    iraise reraise
+
+let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = val_of_named_context (named_context env) in
+  let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
+  let body, eff = Future.force ce.Declare.proof_entry_body in
+  let (cb, ctx) =
+    if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
+    else body
+  in
+  let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
+  cb, status, univs
+
+let refine_by_tactic ~name ~poly env sigma ty tac =
+  (* Save the initial side-effects to restore them afterwards. We set the
+     current set of side-effects to be empty so that we can retrieve the
+     ones created during the tactic invocation easily. *)
+  let eff = Evd.eval_side_effects sigma in
+  let sigma = Evd.drop_side_effects sigma in
+  (* Save the existing goals *)
+  let prev_future_goals = save_future_goals sigma in
+  (* Start a proof *)
+  let prf = Proof.start ~name ~poly sigma [env, ty] in
+  let (prf, _, ()) =
+    try Proof.run_tactic env tac prf
+    with Logic_monad.TacticFailure e as src ->
+      (* Catch the inner error of the monad tactic *)
+      let (_, info) = CErrors.push src in
+      iraise (e, info)
+  in
+  (* Plug back the retrieved sigma *)
+  let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
+  assert (stack = []);
+  let ans = match Proofview.initial_goals entry with
+  | [c, _] -> c
+  | _ -> assert false
+  in
+  let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
+  (* [neff] contains the freshly generated side-effects *)
+  let neff = Evd.eval_side_effects sigma in
+  (* Reset the old side-effects *)
+  let sigma = Evd.drop_side_effects sigma in
+  let sigma = Evd.emit_side_effects eff sigma in
+  (* Restore former goals *)
+  let sigma = restore_future_goals sigma prev_future_goals in
+  (* Push remaining goals as future_goals which is the only way we
+     have to inform the caller that there are goals to collect while
+     not being encapsulated in the monad *)
+  (* Goals produced by tactic "shelve" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+  (* Goals produced by tactic "give_up" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
+  (* Other goals *)
+  let sigma = List.fold_right Evd.declare_future_goal goals sigma in
+  (* Get rid of the fresh side-effects by internalizing them in the term
+     itself. Note that this is unsound, because the tactic may have solved
+     other goals that were already present during its invocation, so that
+     those goals rely on effects that are not present anymore. Hopefully,
+     this hack will work in most cases. *)
+  let neff = neff.Evd.seff_private in
+  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
+  ans, sigma
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
new file mode 100644
index 0000000000..30514191fa
--- /dev/null
+++ b/tactics/pfedit.mli
@@ -0,0 +1,89 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
+
+open Names
+open Constr
+open Environ
+
+(** {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 : Proof_global.t -> int -> Evd.evar_map * env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+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 : 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. [solve SelectAll
+    tac] applies [tac] to all subgoals. *)
+
+val solve : ?with_end_tac:unit Proofview.tactic ->
+      Goal_select.t -> int option -> unit Proofview.tactic ->
+      Proof.t -> Proof.t * bool
+
+(** [by tac] applies tactic [tac] to the 1st subgoal of the current
+    focused proof.
+    Returns [false] if an unsafe tactic has been used. *)
+
+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
+
+(** [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
+    tactic. *)
+
+val build_constant_by_tactic
+  :  name:Id.t
+  -> UState.t
+  -> named_context_val
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Evd.side_effects Declare.proof_entry * bool * UState.t
+
+val build_by_tactic
+  :  ?side_eff:bool
+  -> env
+  -> UState.t
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> constr * bool * UState.t
+
+val refine_by_tactic
+  :  name:Id.t
+  -> poly:bool
+  -> env -> Evd.evar_map
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> constr * Evd.evar_map
+(** A variant of the above function that handles open terms as well.
+    Caveat: all effects are purged in the returned term at the end, but other
+    evars solved by side-effects are NOT purged, so that unexpected failures may
+    occur. Ideally all code using this function should be rewritten in the
+    monad. *)
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
new file mode 100644
index 0000000000..a2929e45cd
--- /dev/null
+++ b/tactics/proof_global.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(***********************************************************************)
+(*                                                                     *)
+(*      This module defines proof facilities relevant to the           *)
+(*      toplevel. In particular it defines the global proof            *)
+(*      environment.                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+open Util
+open Names
+open Context
+
+module NamedDecl = Context.Named.Declaration
+
+(*** Proof Global Environment ***)
+
+type proof_object =
+  { name : Names.Id.t
+  ; entries : Evd.side_effects Declare.proof_entry list
+  ; poly : bool
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
+
+type opacity_flag = Opaque | Transparent
+
+type t =
+  { endline_tactic : Genarg.glob_generic_argument option
+  ; section_vars : Constr.named_context option
+  ; proof : Proof.t
+  ; udecl: UState.universe_decl
+  (** Initial universe declarations *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  }
+
+(*** Proof Global manipulation ***)
+
+let get_proof ps = ps.proof
+let get_proof_name ps = (Proof.data ps.proof).Proof.name
+
+let get_initial_euctx ps = ps.initial_euctx
+
+let map_proof f p = { p with proof = f p.proof }
+let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
+
+let map_fold_proof_endline f ps =
+  let et =
+    match ps.endline_tactic with
+    | None -> Proofview.tclUNIT ()
+    | Some tac ->
+      let open Geninterp in
+      let {Proof.poly} = Proof.data ps.proof in
+      let ist = { lfun = Id.Map.empty; poly; 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, ret
+
+let compact_the_proof pf = map_proof Proof.compact pf
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac ps =
+  { ps with endline_tactic = Some tac }
+
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion). The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+let start_proof ~name ~udecl ~poly sigma goals =
+  let proof = Proof.start ~name ~poly sigma goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
+  ; endline_tactic = None
+  ; section_vars = None
+  ; udecl
+  ; initial_euctx
+  }
+
+let start_dependent_proof ~name ~udecl ~poly goals =
+  let proof = Proof.dependent_start ~name ~poly goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
+  ; endline_tactic = None
+  ; section_vars = None
+  ; udecl
+  ; initial_euctx
+  }
+
+let get_used_variables pf = pf.section_vars
+let get_universe_decl pf = pf.udecl
+
+let set_used_variables ps 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
+  let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe as orig) =
+    match entry with
+    | LocalAssum ({binder_name=x},_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe)
+    | LocalDef ({binder_name=x},bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe)
+       else (ctx, all_safe) in
+  let ctx, _ =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set) 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}
+
+let get_open_goals ps =
+  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+  List.length goals +
+  List.fold_left (+) 0
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
+  List.length shelf
+
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+
+let private_poly_univs =
+  let b = ref true in
+  let _ = Goptions.(declare_bool_option {
+      optdepr = false;
+      optname = "use private polymorphic universes for Qed constants";
+      optkey = ["Private";"Polymorphic";"Universes"];
+      optread = (fun () -> !b);
+      optwrite = ((:=) b);
+    })
+  in
+  fun () -> !b
+
+let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
+                (fpl : closed_proof_output Future.computation) ps =
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let Proof.{ name; poly; entry } = Proof.data proof in
+  let opaque = match opaque with Opaque -> true | Transparent -> false in
+  let constrain_variables ctx =
+    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+  in
+  let fpl, univs = Future.split2 fpl in
+  let universes = if poly || now then Future.force univs else initial_euctx in
+  (* Because of dependent subgoals at the beginning of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k =
+    let { Proof.sigma } = Proof.data proof in
+    Evd.existential_opt_value0 sigma k in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
+    (UState.subst universes) in
+
+  let make_body =
+    if poly || now then
+      let make_body t (c, eff) =
+        let body = c in
+        let allow_deferred =
+          not poly && (keep_body_ucst_separate ||
+          not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
+        in
+        let typ = if allow_deferred then t else nf t in
+        let used_univs_body = Vars.universes_of_constr body in
+        let used_univs_typ = Vars.universes_of_constr typ in
+        if allow_deferred then
+          let initunivs = UState.univ_entry ~poly initial_euctx in
+          let ctx = constrain_variables universes in
+          (* For vi2vo compilation proofs are computed now but we need to
+             complement the univ constraints of the typ with the ones of
+             the body.  So we keep the two sets distinct. *)
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let ctx_body = UState.restrict ctx used_univs in
+          let univs = UState.check_mono_univ_decl ctx_body udecl in
+          (initunivs, typ), ((body, univs), eff)
+        else if poly && opaque && private_poly_univs () then
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let universes = UState.restrict universes used_univs in
+          let typus = UState.restrict universes used_univs_typ in
+          let udecl = UState.check_univ_decl ~poly typus udecl in
+          let ubody = Univ.ContextSet.diff
+              (UState.context_set universes)
+              (UState.context_set typus)
+          in
+          (udecl, typ), ((body, ubody), eff)
+        else
+          (* Since the proof is computed now, we can simply have 1 set of
+             constraints in which we merge the ones for the body and the ones
+             for the typ. We recheck the declaration after restricting with
+             the actually used universes.
+             TODO: check if restrict is really necessary now. *)
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let ctx = UState.restrict universes used_univs in
+          let univs = UState.check_univ_decl ~poly ctx udecl in
+          (univs, typ), ((body, Univ.ContextSet.empty), eff)
+      in
+       fun t p -> Future.split2 (Future.chain p (make_body t))
+    else
+      fun t p ->
+        (* Already checked the univ_decl for the type universes when starting the proof. *)
+        let univctx = UState.univ_entry ~poly:false universes in
+        let t = nf t in
+        Future.from_val (univctx, t),
+        Future.chain p (fun (pt,eff) ->
+          (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+          let univs = Future.force univs in
+          let univs = constrain_variables univs in
+          let used_univs = Univ.LSet.union
+              (Vars.universes_of_constr t)
+              (Vars.universes_of_constr pt)
+          in
+          let univs = UState.restrict univs used_univs in
+          let univs = UState.check_mono_univ_decl univs udecl in
+          (pt,univs),eff)
+  in
+  let entry_fn p (_, t) =
+    let t = EConstr.Unsafe.to_constr t in
+    let univstyp, body = make_body t p in
+    let univs, typ = Future.force univstyp in
+    let open Declare in
+    {
+      proof_entry_body = body;
+      proof_entry_secctx = section_vars;
+      proof_entry_feedback = feedback_id;
+      proof_entry_type  = Some typ;
+      proof_entry_inline_code = false;
+      proof_entry_opaque = opaque;
+      proof_entry_universes = univs; }
+  in
+  let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
+  { name; entries = entries; poly; universes; udecl }
+
+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
+  let eff = Evd.eval_side_effects evd in
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+    proofs, Evd.evar_universe_context evd
+ end else
+  let Proof.{name=pid;entry} = Proof.data proof in
+  let initial_goals = Proofview.initial_goals entry in
+  let evd = Proof.return ~pid proof in
+  let eff = Evd.eval_side_effects evd in
+  let evd = Evd.minimize_universes evd in
+  let proof_opt c =
+    match EConstr.to_constr_opt evd c with
+    | Some p -> p
+    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+  in
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     code-paths that generate several proof entries are derive and
+     equations and so far there is no code in the CI that will
+     actually call those and do a side-effect, TTBOMK *)
+  let proofs =
+    List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
+    proofs, Evd.evar_universe_context evd
+
+let close_future_proof ~opaque ~feedback_id ps 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 =
+  close_proof ~opaque ~keep_body_ucst_separate ~now:true
+    (Future.from_val ~fix_exn (return_proof ps)) ps
+
+let update_global_env =
+  map_proof (fun p ->
+      let { Proof.sigma } = Proof.data p in
+      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)
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
new file mode 100644
index 0000000000..d15e23c2cc
--- /dev/null
+++ b/tactics/proof_global.mli
@@ -0,0 +1,103 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** This module defines proof facilities relevant to the
+     toplevel. In particular it defines the global proof
+     environment. *)
+
+type t
+
+(* Should be moved into a proper view *)
+val get_proof : t -> Proof.t
+val get_proof_name : t -> Names.Id.t
+val get_used_variables : t -> Constr.named_context option
+
+(** Get the universe declaration associated to the current proof. *)
+val get_universe_decl : t -> UState.universe_decl
+
+(** Get initial universe state *)
+val get_initial_euctx : t -> UState.t
+
+val compact_the_proof : t -> t
+
+(** When a proof is closed, it is reified into a [proof_object] *)
+type proof_object =
+  { name : Names.Id.t
+  (** name of the proof *)
+  ; entries : Evd.side_effects Declare.proof_entry list
+  (** list of the proof terms (in a form suitable for definitions). *)
+  ; poly : bool
+  (** polymorphic status *)
+  ; universes: UState.t
+  (** universe state *)
+  ; udecl : UState.universe_decl
+  (** universe declaration *)
+  }
+
+type opacity_flag = Opaque | Transparent
+
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion); [poly] determines if the proof is universe
+   polymorphic. The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+val start_proof
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
+  -> Evd.evar_map
+  -> (Environ.env * EConstr.types) list
+  -> t
+
+(** Like [start_proof] except that there may be dependencies between
+    initial goals. *)
+val start_dependent_proof
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
+  -> Proofview.telescope
+  -> 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 : t -> t
+
+(* Takes a function to add to the exceptions data relative to the
+   state in which the proof was built *)
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object
+
+(* Intermediate step necessary to delegate the future.
+ * Both access the current proof state. The former is supposed to be
+ * chained with a computation that completed the proof *)
+
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+
+(* 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 -> t -> closed_proof_output
+val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
+  closed_proof_output Future.computation -> proof_object
+
+val get_open_goals : t -> int
+
+val map_proof : (Proof.t -> Proof.t) -> t -> t
+val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
+val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+
+(** Sets the tactic to be used when a tactic line is closed with [...] *)
+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 : t ->
+  Names.Id.t list -> (Constr.named_context * Names.lident list) * t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 6dd749aa0d..c5c7969a09 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,4 +1,6 @@
 Declare
+Proof_global
+Pfedit
 Dnet
 Dn
 Btermdn