[proof] Merge `Proof_global` into `Declare`

We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]

Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.

8 files changed, 534 insertions, 554 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 8abd68d28d..ac16a2c591 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -91,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context sigma in
   let (const, safe, ectx) =
-    try Proof_global.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
+    try Declare.build_constant_by_tactic ~name ~opaque:Declare.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -106,7 +106,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   (* EJGA: Hack related to the above call to
      `build_constant_by_tactic` with `~opaque:Transparent`. Even if
      the abstracted term is destined to be opaque, if we trigger the
-     `if poly && opaque && private_poly_univs ()` in `Proof_global`
+     `if poly && opaque && private_poly_univs ()` in `Declare`
      kernel will boom. This deserves more investigation. *)
   let const = Declare.Internal.set_opacity ~opaque const in
   let const, args = Declare.Internal.shrink_entry sign const in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 5135d72f7b..f8c10c5370 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -13,11 +13,112 @@
 open Pp
 open Util
 open Names
-open Declarations
-open Entries
 open Safe_typing
-open Libobject
-open Lib
+module NamedDecl = Context.Named.Declaration
+
+type opacity_flag = Opaque | Transparent
+
+type t =
+  { endline_tactic : Genarg.glob_generic_argument option
+  ; section_vars : Id.Set.t 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 ({Context.binder_name=x},_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe)
+    | LocalDef ({Context.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");
+  ctx, { ps with section_vars = Some (Context.Named.to_vars 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
 
 (* object_kind , id *)
 exception AlreadyDeclared of (string option * Id.t)
@@ -30,8 +131,6 @@ let _ = CErrors.register_handler (function
     | _ ->
       None)
 
-module NamedDecl = Context.Named.Declaration
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Monomorphic universes need to survive sections. *)
@@ -78,10 +177,118 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
+let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
+
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
+  { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
+    proof_entry_secctx = section_vars;
+    proof_entry_type = types;
+    proof_entry_universes = univs;
+    proof_entry_opaque = opaque;
+    proof_entry_feedback = feedback_id;
+    proof_entry_inline_code = inline}
+
+type proof_object =
+  { name : Names.Id.t
+  (* [name] only used in the STM *)
+  ; entries : Evd.side_effects proof_entry list
+  ; uctx: UState.t
+  }
+
+let private_poly_univs =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Private";"Polymorphic";"Universes"]
+    ~value:true
+
+(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
+(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
+let prepare_proof ~unsafe_typ { proof } =
+  let Proof.{name=pid;entry;poly} = 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 to_constr_body c =
+    match EConstr.to_constr_opt evd c with
+    | Some p -> p
+    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+  in
+  let to_constr_typ t =
+    if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
+  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 *)
+  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
+  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
+  proofs, Evd.evar_universe_context evd
+
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { Proof.name; poly } = Proof.data proof in
+  let unsafe_typ = keep_body_ucst_separate && not poly in
+  let elist, uctx = prepare_proof ~unsafe_typ ps in
+  let opaque = match opaque with Opaque -> true | Transparent -> false in
+
+  let make_entry ((body, eff), typ) =
+
+    let allow_deferred =
+      not poly &&
+      (keep_body_ucst_separate
+       || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+    in
+    let used_univs_body = Vars.universes_of_constr body in
+    let used_univs_typ = Vars.universes_of_constr typ in
+    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+    let utyp, ubody =
+      if allow_deferred then
+        let utyp = UState.univ_entry ~poly initial_euctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx 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 uctx_body = UState.restrict uctx used_univs in
+        let ubody = UState.check_mono_univ_decl uctx_body udecl in
+        utyp, ubody
+      else if poly && opaque && private_poly_univs () then
+        let universes = UState.restrict uctx used_univs in
+        let typus = UState.restrict universes used_univs_typ in
+        let utyp = UState.check_univ_decl ~poly typus udecl in
+        let ubody = Univ.ContextSet.diff
+            (UState.context_set universes)
+            (UState.context_set typus)
+        in
+        utyp, ubody
+      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 ctx = UState.restrict uctx used_univs in
+        let utyp = UState.check_univ_decl ~poly ctx udecl in
+        utyp, Univ.ContextSet.empty
+    in
+    definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+  in
+  let entries = CList.map make_entry elist  in
+  { name; entries; uctx }
+
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
-  | ParameterEntry of parameter_entry
-  | PrimitiveEntry of primitive_entry
+  | ParameterEntry of Entries.parameter_entry
+  | PrimitiveEntry of Entries.primitive_entry
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -99,7 +306,7 @@ let open_constant f i ((sp,kn), obj) =
   | ImportNeedQualified -> ()
   | ImportDefaultBehavior ->
     let con = Global.constant_of_delta_kn kn in
-    if in_filter_ref (GlobRef.ConstRef con) f then
+    if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
       Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
 
 let exists_name id =
@@ -130,9 +337,10 @@ let dummy_constant cst = {
   cst_locl = cst.cst_locl;
 }
 
-let classify_constant cst = Substitute (dummy_constant cst)
+let classify_constant cst = Libobject.Substitute (dummy_constant cst)
 
 let (objConstant : constant_obj Libobject.Dyn.tag) =
+  let open Libobject in
   declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -153,7 +361,7 @@ let register_constant kn kind local =
     cst_locl = local;
   } in
   let id = Label.to_id (Constant.label kn) in
-  let _ = add_leaf id o in
+  let _ = Lib.add_leaf id o in
   update_tables kn
 
 let register_side_effect (c, role) =
@@ -186,18 +394,6 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
-
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
-    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
-  { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
-    proof_entry_secctx = section_vars;
-    proof_entry_type = types;
-    proof_entry_universes = univs;
-    proof_entry_opaque = opaque;
-    proof_entry_feedback = feedback_id;
-    proof_entry_inline_code = inline}
-
 let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) body =
   { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
@@ -223,14 +419,13 @@ let cast_proof_entry e =
   let univs =
     if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
     else match e.proof_entry_universes with
-      | Monomorphic_entry ctx' ->
+      | Entries.Monomorphic_entry ctx' ->
         (* This can actually happen, try compiling EqdepFacts for instance *)
-        Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
-      | Polymorphic_entry _ ->
+        Entries.Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
+      | Entries.Polymorphic_entry _ ->
         CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
   in
-  {
-    const_entry_body = body;
+  { Entries.const_entry_body = body;
     const_entry_secctx = e.proof_entry_secctx;
     const_entry_feedback = e.proof_entry_feedback;
     const_entry_type = e.proof_entry_type;
@@ -242,7 +437,7 @@ type ('a, 'b) effect_entry =
 | EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry
 | PureEntry : (unit, Constr.constr) effect_entry
 
-let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry =
+let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b Entries.opaque_entry =
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -276,16 +471,16 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
   | PureEntry ->
     let (body, uctx), () = Future.force e.proof_entry_body in
     let univs = match e.proof_entry_universes with
-    | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx')
-    | Polymorphic_entry _ ->
+    | Entries.Monomorphic_entry uctx' ->
+      Entries.Monomorphic_entry (Univ.ContextSet.union uctx uctx')
+    | Entries.Polymorphic_entry _ ->
       assert (Univ.ContextSet.is_empty uctx);
       e.proof_entry_universes
     in
     body, univs
   | EffectEntry -> e.proof_entry_body, e.proof_entry_universes
   in
-  {
-    opaque_entry_body = body;
+  { Entries.opaque_entry_body = body;
     opaque_entry_secctx = secctx;
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
@@ -295,6 +490,7 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
 let is_unsafe_typing_flags () =
+  let open Declarations in
   let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
@@ -366,6 +562,7 @@ type variable_declaration =
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
 let objVariable : unit Libobject.Dyn.tag =
+  let open Libobject in
   declare_object_full { (default_object "VARIABLE") with
     classify_function = (fun () -> Dispose)}
 
@@ -386,15 +583,15 @@ let declare_variable ~name ~kind d =
       let ((body, body_ui), eff) = Future.force de.proof_entry_body in
       let () = export_side_effects eff in
       let poly, entry_ui = match de.proof_entry_universes with
-        | Monomorphic_entry uctx -> false, uctx
-        | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+        | Entries.Monomorphic_entry uctx -> false, uctx
+        | Entries.Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union body_ui entry_ui in
       (* We must declare the universe constraints before type-checking the
          term. *)
       let () = declare_universe_context ~poly univs in
       let se = {
-        secdef_body = body;
+        Entries.secdef_body = body;
         secdef_secctx = de.proof_entry_secctx;
         secdef_feedback = de.proof_entry_feedback;
         secdef_type = de.proof_entry_type;
@@ -404,7 +601,7 @@ let declare_variable ~name ~kind d =
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
-  ignore(add_leaf name (inVariable ()) : Libobject.object_name);
+  ignore(Lib.add_leaf name (inVariable ()) : Libobject.object_name);
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
@@ -511,3 +708,142 @@ module Internal = struct
   let objConstant = objConstant
 
 end
+(*** Proof Global Environment ***)
+
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+
+let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { Proof.name; poly; entry; sigma } = Proof.data proof in
+
+  (* We don't allow poly = true in this path *)
+  if poly then
+    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
+
+  let fpl, uctx = Future.split2 fpl 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 = Evd.existential_opt_value0 sigma k in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
+
+  (* We only support opaque proofs, this will be enforced by using
+     different entries soon *)
+  let opaque = true in
+  let make_entry p (_, types) =
+    (* Already checked the univ_decl for the type universes when starting the proof. *)
+    let univs = UState.univ_entry ~poly:false initial_euctx in
+    let types = nf (EConstr.Unsafe.to_constr types) in
+
+    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 uctx = Future.force uctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+        let used_univs = Univ.LSet.union
+            (Vars.universes_of_constr types)
+            (Vars.universes_of_constr pt)
+        in
+        let univs = UState.restrict uctx used_univs in
+        let univs = UState.check_mono_univ_decl univs udecl in
+        (pt,univs),eff)
+    |> delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types
+  in
+  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
+  { name; entries; uctx = initial_euctx }
+
+let close_future_proof = close_proof_delayed
+
+let return_partial_proof { proof } =
+ 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
+
+let return_proof ps =
+  let p, uctx = prepare_proof ~unsafe_typ:false ps in
+  List.map fst p, uctx
+
+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)
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let by tac = map_fold_proof (Pfedit.solve (Goal_select.SelectNth 1) None tac)
+
+let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
+  let evd = Evd.from_ctx uctx in
+  let goals = [ (Global.env_of_context sign , typ) ] in
+  let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
+  let pf, status = by tac pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
+  match entries with
+  | [entry] ->
+    entry, status, uctx
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
+
+let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = Environ.(val_of_named_context (named_context env)) in
+  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+  let cb, uctx =
+    if side_eff then inline_private_constants ~uctx env ce
+    else
+      (* GG: side effects won't get reset: no need to treat their universes specially *)
+      let (cb, ctx), _eff = Future.force ce.proof_entry_body in
+      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
+  in
+  cb, ce.proof_entry_type, status, univs
+
+exception NoSuchGoal
+let () = CErrors.register_handler begin function
+  | NoSuchGoal -> Some Pp.(str "No such goal.")
+  | _ -> None
+end
+
+let get_nth_V82_goal p i =
+  let Proof.{ sigma; goals } = Proof.data p in
+  try { Evd.it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise NoSuchGoal
+
+let get_goal_context_gen pf i =
+  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+  (sigma, Refiner.pf_env { Evd.it=goal ; sigma=sigma; })
+
+let get_goal_context pf i =
+  let p = get_proof pf in
+  get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = 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_proof_context p =
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal ->
+    (* No more focused goals *)
+    let { Proof.sigma } = Proof.data p in
+    sigma, Global.env ()
+
+let get_current_context pf =
+  let p = get_proof pf in
+  get_proof_context p
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 615cffeae7..cf6748282c 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -12,14 +12,85 @@ open Names
 open Constr
 open Entries
 
-(** This module provides the official functions to declare new variables,
-   parameters, constants and inductive types. Using the following functions
-   will add the entries in the global environment (module [Global]), will
-   register the declarations in the library (module [Lib]) --- so that the
-   reset works properly --- and will fill some global tables such as
-   [Nametab] and [Impargs]. *)
-
-(** Proof entries *)
+(** This module provides the official functions to declare new
+   variables, parameters, constants and inductive types in the global
+   environment. It also updates some accesory tables such as [Nametab]
+   (name resolution), [Impargs], and [Notations]. *)
+
+(** We provide two kind of fuctions:
+
+  - one go functions, that will register a constant in one go, suited
+   for non-interactive definitions where the term is given.
+
+  - two-phase [start/declare] functions which will create an
+   interactive proof, allow its modification, and saving when
+   complete.
+
+  Internally, these functions mainly differ in that usually, the first
+  case doesn't require setting up the tactic engine.
+
+ *)
+
+(** [Declare.t] Interactive, unsaved constant/proof. *)
+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 -> Names.Id.Set.t 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
+
+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) *)
+val set_used_variables : t ->
+  Names.Id.t list -> Constr.named_context * t
+
+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
+
+(** Proof entries represent a proof that has been finished, but still
+   not registered with the kernel. *)
 type 'a proof_entry = private {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
@@ -32,6 +103,18 @@ type 'a proof_entry = private {
   proof_entry_inline_code : bool;
 }
 
+(** 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 proof_entry list
+  (** list of the proof terms (in a form suitable for definitions). *)
+  ; uctx: UState.t
+  (** universe state *)
+  }
+
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
+
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type variable_declaration =
@@ -157,3 +240,69 @@ module Internal : sig
   val objVariable : unit Libobject.Dyn.tag
 
 end
+
+(* 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
+
+(** Requires a complete proof. *)
+val return_proof : t -> closed_proof_output
+
+(** An incomplete proof is allowed (no error), and a warn is given if
+   the proof is complete. *)
+val return_partial_proof : t -> closed_proof_output
+val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
+
+val get_open_goals : t -> int
+
+(** [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 -> t -> t * 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:Names.Id.t
+  -> ?opaque:opacity_flag
+  -> uctx:UState.t
+  -> sign:Environ.named_context_val
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Evd.side_effects proof_entry * bool * UState.t
+
+val build_by_tactic
+  :  ?side_eff:bool
+  -> Environ.env
+  -> uctx:UState.t
+  -> poly:bool
+  -> typ:EConstr.types
+  -> unit Proofview.tactic
+  -> Constr.constr * Constr.types option * bool * UState.t
+
+(** {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 : t -> int -> Evd.evar_map * Environ.env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+val get_current_goal_context : t -> Evd.evar_map * Environ.env
+
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_context : Proof.t -> Evd.evar_map * Environ.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 : t -> Evd.evar_map * Environ.env
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2118b4f231..a2edafb376 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1562,7 +1562,7 @@ let pr_hint_term env sigma cl =
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Proof_global.get_proof pf in
+  let pts = Declare.get_proof pf in
   let Proof.{goals;sigma} = Proof.data pts in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9e11931247..7f870964ab 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -306,7 +306,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Proof_global.t -> Pp.t
+val pr_applicable_hint : Declare.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
deleted file mode 100644
index 78691d8c74..0000000000
--- a/tactics/proof_global.ml
+++ /dev/null
@@ -1,355 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \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 Util
-open Names
-open Context
-
-module NamedDecl = Context.Named.Declaration
-
-(*** Proof Global Environment ***)
-
-type proof_object =
-  { name : Names.Id.t
-  (* [name] only used in the STM *)
-  ; entries : Evd.side_effects Declare.proof_entry list
-  ; uctx: UState.t
-  }
-
-type opacity_flag = Opaque | Transparent
-
-type t =
-  { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Id.Set.t 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");
-  ctx, { ps with section_vars = Some (Context.Named.to_vars 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 =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Private";"Polymorphic";"Universes"]
-    ~value:true
-
-(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
-(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
-let prepare_proof ~unsafe_typ { proof } =
-  let Proof.{name=pid;entry;poly} = 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 to_constr_body c =
-    match EConstr.to_constr_opt evd c with
-    | Some p -> p
-    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
-  in
-  let to_constr_typ t =
-    if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
-  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 *)
-  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
-  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
-  proofs, Evd.evar_universe_context evd
-
-let close_proof ~opaque ~keep_body_ucst_separate ps =
-
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly } = Proof.data proof in
-  let unsafe_typ = keep_body_ucst_separate && not poly in
-  let elist, uctx = prepare_proof ~unsafe_typ ps in
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
-
-  let make_entry ((body, eff), typ) =
-
-    let allow_deferred =
-      not poly &&
-      (keep_body_ucst_separate
-       || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
-    in
-    let used_univs_body = Vars.universes_of_constr body in
-    let used_univs_typ = Vars.universes_of_constr typ in
-    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-    let utyp, ubody =
-      if allow_deferred then
-        let utyp = UState.univ_entry ~poly initial_euctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx 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 uctx_body = UState.restrict uctx used_univs in
-        let ubody = UState.check_mono_univ_decl uctx_body udecl in
-        utyp, ubody
-      else if poly && opaque && private_poly_univs () then
-        let universes = UState.restrict uctx used_univs in
-        let typus = UState.restrict universes used_univs_typ in
-        let utyp = UState.check_univ_decl ~poly typus udecl in
-        let ubody = Univ.ContextSet.diff
-            (UState.context_set universes)
-            (UState.context_set typus)
-        in
-        utyp, ubody
-      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 ctx = UState.restrict uctx used_univs in
-        let utyp = UState.check_univ_decl ~poly ctx udecl in
-        utyp, Univ.ContextSet.empty
-    in
-    Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
-  in
-  let entries = CList.map make_entry elist  in
-  { name; entries; uctx }
-
-let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly; entry; sigma } = Proof.data proof in
-
-  (* We don't allow poly = true in this path *)
-  if poly then
-    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
-
-  let fpl, uctx = Future.split2 fpl 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 = Evd.existential_opt_value0 sigma k in
-  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
-
-  (* We only support opaque proofs, this will be enforced by using
-     different entries soon *)
-  let opaque = true in
-  let make_entry p (_, types) =
-    (* Already checked the univ_decl for the type universes when starting the proof. *)
-    let univs = UState.univ_entry ~poly:false initial_euctx in
-    let types = nf (EConstr.Unsafe.to_constr types) in
-
-    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 uctx = Future.force uctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-        let used_univs = Univ.LSet.union
-            (Vars.universes_of_constr types)
-            (Vars.universes_of_constr pt)
-        in
-        let univs = UState.restrict uctx used_univs in
-        let univs = UState.check_mono_univ_decl univs udecl in
-        (pt,univs),eff)
-    |> Declare.delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types
-  in
-  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx = initial_euctx }
-
-let close_future_proof = close_proof_delayed
-
-let return_partial_proof { proof } =
- 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
-
-let return_proof ps =
-  let p, uctx = prepare_proof ~unsafe_typ:false ps in
-  List.map fst p, uctx
-
-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)
-
-let next = let n = ref 0 in fun () -> incr n; !n
-
-let by tac = map_fold_proof (Pfedit.solve (Goal_select.SelectNth 1) None tac)
-
-let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
-  let evd = Evd.from_ctx uctx in
-  let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
-  let pf, status = by tac pf in
-  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
-  match entries with
-  | [entry] ->
-    entry, status, uctx
-  | _ ->
-    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
-
-let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
-  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = Environ.(val_of_named_context (named_context env)) in
-  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
-  let cb, uctx =
-    if side_eff then Declare.inline_private_constants ~uctx env ce
-    else
-      (* GG: side effects won't get reset: no need to treat their universes specially *)
-      let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
-      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
-  in
-  cb, ce.Declare.proof_entry_type, status, univs
-
-exception NoSuchGoal
-let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Some Pp.(str "No such goal.")
-  | _ -> None
-end
-
-let get_nth_V82_goal p i =
-  let Proof.{ sigma; goals } = Proof.data p in
-  try { Evd.it = List.nth goals (i-1) ; sigma }
-  with Failure _ -> raise NoSuchGoal
-
-let get_goal_context_gen pf i =
-  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
-  (sigma, Refiner.pf_env { Evd.it=goal ; sigma=sigma; })
-
-let get_goal_context pf i =
-  let p = get_proof pf in
-  get_goal_context_gen p i
-
-let get_current_goal_context pf =
-  let p = 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_proof_context p =
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* No more focused goals *)
-    let { Proof.sigma } = Proof.data p in
-    sigma, Global.env ()
-
-let get_current_context pf =
-  let p = get_proof pf in
-  get_proof_context p
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
deleted file mode 100644
index c41a9c656e..0000000000
--- a/tactics/proof_global.mli
+++ /dev/null
@@ -1,149 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \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)         *)
-(************************************************************************)
-
-(** State for interactive proofs. *)
-
-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 -> Names.Id.Set.t 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). *)
-  ; uctx: UState.t
-  (** universe state *)
-  }
-
-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 -> 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
-
-(** Requires a complete proof. *)
-val return_proof : t -> closed_proof_output
-
-(** An incomplete proof is allowed (no error), and a warn is given if
-   the proof is complete. *)
-val return_partial_proof : t -> closed_proof_output
-val close_future_proof : 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) *)
-val set_used_variables : t ->
-  Names.Id.t list -> Constr.named_context * t
-
-(** [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 -> t -> t * 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:Names.Id.t
-  -> ?opaque:opacity_flag
-  -> uctx:UState.t
-  -> sign:Environ.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
-  -> Environ.env
-  -> uctx:UState.t
-  -> poly:bool
-  -> typ:EConstr.types
-  -> unit Proofview.tactic
-  -> Constr.constr * Constr.types option * bool * UState.t
-
-(** {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 : t -> int -> Evd.evar_map * Environ.env
-
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : t -> Evd.evar_map * Environ.env
-
-(** [get_proof_context ()] gets the goal context for the first subgoal
-    of the proof *)
-val get_proof_context : Proof.t -> Evd.evar_map * Environ.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 : t -> Evd.evar_map * Environ.env
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index f9f2a78c35..d1865c974c 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,7 +1,6 @@
 DeclareScheme
 Pfedit
 Declare
-Proof_global
 Dnet
 Dn
 Btermdn