From e04377e2c5eca2b47bd5f8db320069aa47040488 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Apr 2020 22:58:40 -0400
Subject: [declare] [tactics] Move declare to `vernac`

This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.

There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:

- moved leminv to `ltac_plugin`; this is unused in the core codebase
  and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
  later, for now I've introduced a `declareUctx` module to avoid being
  invasive there.

In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.

This partially supersedes #10951 for now and helps with #11492 .
---
 dev/base_include                |   2 +-
 plugins/ltac/extratactics.mlg   |   2 +-
 plugins/ltac/leminv.ml          | 297 +++++++++++++
 plugins/ltac/leminv.mli         |  21 +
 plugins/ltac/ltac_plugin.mlpack |   1 +
 plugins/setoid_ring/newring.ml  |   2 +-
 tactics/abstract.ml             |   5 +-
 tactics/abstract.mli            |  12 +
 tactics/declare.ml              | 901 ----------------------------------------
 tactics/declare.mli             | 314 --------------
 tactics/declareUctx.ml          |  34 ++
 tactics/declareUctx.mli         |  11 +
 tactics/hints.ml                |   5 +-
 tactics/hints.mli               |   2 +-
 tactics/ind_tables.ml           |   8 +-
 tactics/ind_tables.mli          |   8 +
 tactics/leminv.ml               | 297 -------------
 tactics/leminv.mli              |  21 -
 tactics/tactics.mllib           |   3 +-
 vernac/comAssumption.ml         |   6 +-
 vernac/comHints.ml              |   2 +-
 vernac/declare.ml               | 886 +++++++++++++++++++++++++++++++++++++++
 vernac/declare.mli              | 299 +++++++++++++
 vernac/declareUniv.ml           |   4 +-
 vernac/vernac.mllib             |   1 +
 vernac/vernacentries.ml         |   3 +-
 26 files changed, 1593 insertions(+), 1554 deletions(-)
 create mode 100644 plugins/ltac/leminv.ml
 create mode 100644 plugins/ltac/leminv.mli
 delete mode 100644 tactics/declare.ml
 delete mode 100644 tactics/declare.mli
 create mode 100644 tactics/declareUctx.ml
 create mode 100644 tactics/declareUctx.mli
 delete mode 100644 tactics/leminv.ml
 delete mode 100644 tactics/leminv.mli
 create mode 100644 vernac/declare.ml
 create mode 100644 vernac/declare.mli

diff --git a/dev/base_include b/dev/base_include
index 96a867475d..45e79147c1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -129,7 +129,7 @@ open Elim
 open Equality
 open Hipattern
 open Inv
-open Leminv
+open Ltac_plugin.Leminv
 open Tacticals
 open Tactics
 open Eqschemes
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7754fe401e..0bad3cbe5b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
         else (* This is a global universe context that shouldn't be
                 refreshed at every use of the hint, declare it globally. *)
-          (Declare.declare_universe_context ~poly:false ctx;
+          (DeclareUctx.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
new file mode 100644
index 0000000000..5a8ec404ee
--- /dev/null
+++ b/plugins/ltac/leminv.ml
@@ -0,0 +1,297 @@
+(************************************************************************)
+(*         *   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 Pp
+open CErrors
+open Util
+open Names
+open Termops
+open Environ
+open Constr
+open Context
+open EConstr
+open Vars
+open Namegen
+open Evd
+open Printer
+open Reductionops
+open Inductiveops
+open Tacmach.New
+open Clenv
+open Tacticals.New
+open Tactics
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+let no_inductive_inconstr env sigma constr =
+  (str "Cannot recognize an inductive predicate in " ++
+     pr_leconstr_env env sigma constr ++
+     str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
+     spc () ++ str "or of the type of constructors" ++ spc () ++
+     str "is hidden by constant definitions.")
+
+(* Inversion stored in lemmas *)
+
+(* ALGORITHM:
+
+   An inversion stored in a lemma is computed from a term-pattern, in
+   a signature, as follows:
+
+   Suppose we have an inductive relation, (I abar), in a signature Gamma:
+
+       Gamma |- (I abar)
+
+   Then we compute the free-variables of abar.  Suppose that Gamma is
+   thinned out to only include these.
+
+   [We need technically to require that all free-variables of the
+    types of the free variables of abar are themselves free-variables
+    of abar.  This needs to be checked, but it should not pose a
+    problem - it is hard to imagine cases where it would not hold.]
+
+   Now, we pose the goal:
+
+       (P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]).
+
+   We execute the tactic:
+
+   REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME))
+
+   This leaves us with some subgoals.  All the assumptions after "P"
+   in these subgoals are new assumptions.  I.e. if we have a subgoal,
+
+       P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar)
+
+   then the assumption we needed to have was
+
+      (Hbar:Tbar)(P ybar)
+
+   So we construct all the assumptions we need, and rebuild the goal
+   with these assumptions.  Then, we can re-apply the same tactic as
+   above, but instead of stopping after the inversion, we just apply
+   the respective assumption in each subgoal.
+
+ *)
+
+(* returns the sub_signature of sign corresponding to those identifiers that
+ * are not global. *)
+(*
+let get_local_sign sign =
+  let lid = ids_of_sign sign in
+  let globsign = Global.named_context() in
+  let add_local id res_sign =
+    if not (mem_sign globsign id) then
+      add_sign (lookup_sign id sign) res_sign
+    else
+      res_sign
+  in
+  List.fold_right add_local lid nil_sign
+*)
+(* returns the identifier of lid that was the latest declared in sign.
+ * (i.e. is the identifier id of lid such that
+ * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
+ * for any id'<>id in lid).
+ * it returns both the pair (id,(sign_prefix id sign)) *)
+(*
+let max_prefix_sign lid sign =
+  let rec max_rec (resid,prefix) = function
+    | [] -> (resid,prefix)
+    | (id::l) ->
+        let pre = sign_prefix id sign in
+        if sign_length pre > sign_length prefix then
+          max_rec (id,pre) l
+        else
+          max_rec (resid,prefix) l
+  in
+  match lid with
+    | [] -> nil_sign
+    | id::l -> snd (max_rec (id, sign_prefix id sign) l)
+*)
+let rec add_prods_sign env sigma t =
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Prod (na,c1,b) ->
+        let id = id_of_name_using_hdchar env sigma t na.binder_name in
+        let b'= subst1 (mkVar id) b in
+        add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
+    | LetIn (na,c1,t1,b) ->
+        let id = id_of_name_using_hdchar env sigma t na.binder_name in
+        let b'= subst1 (mkVar id) b in
+        add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
+    | _ -> (env,t)
+
+(* [dep_option] indicates whether the inversion lemma is dependent or not.
+   If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
+   the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
+   where P:(x_bar:T_bar)(H:(I x_bar))[sort].
+   The generalisation of such a goal at the moment of the dependent case should
+   be easy.
+
+   If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the
+   variables occurring in [I], then the stated goal will be:
+    (x_bar:T_bar)(I t_bar)->(P x_bar)
+   where P: P:(x_bar:T_bar)[sort].
+*)
+
+let compute_first_inversion_scheme env sigma ind sort dep_option =
+  let indf,realargs = dest_ind_type ind in
+  let allvars = vars_of_env env in
+  let p = next_ident_away (Id.of_string "P") allvars in
+  let pty,goal =
+    if dep_option  then
+      let pty = make_arity env sigma true indf sort in
+      let r = relevance_of_inductive_type env ind in
+      let goal =
+        mkProd
+          (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
+      in
+      pty,goal
+    else
+      let i = mkAppliedInd ind in
+      let ivars = global_vars env sigma i in
+      let revargs,ownsign =
+        fold_named_context
+          (fun env d (revargs,hyps) ->
+            let d = map_named_decl EConstr.of_constr d in
+             let id = NamedDecl.get_id d in
+             if Id.List.mem id ivars then
+               ((mkVar id)::revargs, Context.Named.add d hyps)
+             else
+               (revargs,hyps))
+          env ~init:([],[])
+      in
+      let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
+      let goal = mkArrow i Sorts.Relevant (applist(mkVar p, List.rev revargs)) in
+      (pty,goal)
+  in
+  let npty = nf_all env sigma pty in
+  let extenv = push_named (LocalAssum (make_annot p Sorts.Relevant,npty)) env in
+  extenv, goal
+
+(* [inversion_scheme sign I]
+
+   Given a local signature, [sign], and an instance of an inductive
+   relation, [I], inversion_scheme will prove the associated inversion
+   scheme on sort [sort]. Depending on the value of [dep_option] it will
+   build a dependent lemma or a non-dependent one *)
+
+let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
+  let (env,i) = add_prods_sign env sigma t in
+  let ind =
+    try find_rectype env sigma i
+    with Not_found ->
+      user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
+  in
+  let (invEnv,invGoal) =
+    compute_first_inversion_scheme env sigma ind sort dep_option
+  in
+  assert
+    (List.subset
+       (global_vars env sigma invGoal)
+       (ids_of_named_context (named_context invEnv)));
+  (*
+    user_err ~hdr:"lemma_inversion"
+    (str"Computed inversion goal was not closed in initial signature.");
+  *)
+  let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
+  let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
+  let pfterm = List.hd (Proof.partial_proof pf) in
+  let global_named_context = Global.named_context_val () in
+  let ownSign = ref begin
+    fold_named_context
+      (fun env d sign ->
+        let d = map_named_decl EConstr.of_constr d in
+         if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
+         else Context.Named.add d sign)
+      invEnv ~init:Context.Named.empty
+  end in
+  let avoid = ref Id.Set.empty in
+  let Proof.{sigma} = Proof.data pf in
+  let sigma = Evd.minimize_universes sigma in
+  let rec fill_holes c =
+    match EConstr.kind sigma c with
+    | Evar (e,args) ->
+        let h = next_ident_away (Id.of_string "H") !avoid in
+        let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
+        avoid := Id.Set.add h !avoid;
+        ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
+        applist (mkVar h, inst)
+    | _ -> EConstr.map sigma fill_holes c
+  in
+  let c = fill_holes pfterm in
+  (* warning: side-effect on ownSign *)
+  let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+  let p = EConstr.to_constr sigma invProof in
+  p, sigma
+
+let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
+  let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
+  let univs = Evd.univ_entry ~poly sigma in
+  let entry = Declare.definition_entry ~univs invProof in
+  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+  ()
+
+(* inv_op = Inv (derives de complete inv. lemma)
+ * inv_op = InvNoThining (derives de semi inversion lemma) *)
+
+let add_inversion_lemma_exn ~poly na com comsort bool tac =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
+  let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
+  try
+    add_inversion_lemma ~poly na env sigma c sort bool tac
+  with
+    |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
+          user_err ~hdr:"Inv needs Nodep Prop Set" s
+
+(* ================================= *)
+(* Applying a given inversion lemma  *)
+(* ================================= *)
+
+let lemInv id c =
+  Proofview.Goal.enter begin fun gls ->
+  try
+    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
+    let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
+    Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
+  with
+    | NoSuchBinding ->
+        user_err
+          (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+    | UserError (a,b) ->
+         user_err ~hdr:"LemInv"
+           (str "Cannot refine current goal with the lemma " ++
+              pr_leconstr_env (pf_env gls) (project gls) c)
+  end
+
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
+
+let lemInvIn id c ids =
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
+    let intros_replace_ids =
+      let concl = Proofview.Goal.concl gl in
+      let sigma = project gl in
+      let nb_of_new_hyp = nb_prod sigma concl - List.length ids in
+      if nb_of_new_hyp < 1  then
+        intros_replacing ids
+      else
+        (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
+    in
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
+        (intros_replace_ids)))
+  end
+
+let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
+
+let lemInv_clause id c = function
+  | [] -> lemInv_gen id c
+  | l -> lemInvIn_gen id c l
diff --git a/plugins/ltac/leminv.mli b/plugins/ltac/leminv.mli
new file mode 100644
index 0000000000..5a5de7b58f
--- /dev/null
+++ b/plugins/ltac/leminv.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*         *   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 Names
+open EConstr
+open Constrexpr
+open Tactypes
+
+val lemInv_clause :
+  quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
+
+val add_inversion_lemma_exn : poly:bool ->
+  Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
+    unit
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index e83eab20dc..f31361279c 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -9,6 +9,7 @@ Tactic_debug
 Tacintern
 Profile_ltac
 Tactic_matching
+Leminv
 Tacinterp
 Tacentries
 Evar_tactics
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0646af3552..633cdbd735 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -150,7 +150,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
-  let () = Declare.declare_universe_context ~poly:false univs in
+  let () = DeclareUctx.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant ~name:(Id.of_string na)
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 0e78a03f45..6b575d0807 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -40,6 +40,9 @@ let name_op_to_name ~name_op ~name suffix =
   | Some s -> s
   | None -> Nameops.add_suffix name suffix
 
+let declare_abstract = ref (fun ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl ->
+  CErrors.anomaly (Pp.str "Abstract declaration hook not registered"))
+
 let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
@@ -77,7 +80,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let concl = it_mkNamedProd_or_LetIn concl sign in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let effs, sigma, lem, args, safe =
-    Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
+    !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 5c936ff9d6..a138a457b3 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,15 @@ val cache_term_by_tactic_then
   -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+val declare_abstract :
+  (  name:Names.Id.t
+  -> poly:bool
+  -> kind:Decls.logical_kind
+  -> sign:EConstr.named_context
+  -> secsign:Environ.named_context_val
+  -> opaque:bool
+  -> solve_tac:unit Proofview.tactic
+  -> Evd.evar_map
+  -> EConstr.t
+  -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool) ref
diff --git a/tactics/declare.ml b/tactics/declare.ml
deleted file mode 100644
index cce43e833e..0000000000
--- a/tactics/declare.ml
+++ /dev/null
@@ -1,901 +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)         *)
-(************************************************************************)
-
-(** This module is about the low-level declaration of logical objects *)
-
-open Pp
-open Util
-open Names
-open Safe_typing
-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)
-
-let _ = CErrors.register_handler (function
-    | AlreadyDeclared (kind, id) ->
-      Some
-        (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
-             ; Id.print id; str " already exists."])
-    | _ ->
-      None)
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-(** Monomorphic universes need to survive sections. *)
-
-let name_instance inst =
-  let map lvl = match Univ.Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        Name (Libnames.qualid_basename qid)
-      with Not_found ->
-        (* Best-effort naming from the string representation of the level.
-           See univNames.ml for a similar hack. *)
-        Name (Id.of_string_soft (Univ.Level.to_string lvl))
-  in
-  Array.map map (Univ.Instance.to_array inst)
-
-let declare_universe_context ~poly ctx =
-  if poly then
-    let uctx = Univ.ContextSet.to_context ctx in
-    let nas = name_instance (Univ.UContext.instance uctx) in
-    Global.push_section_context (nas, uctx)
-  else
-    Global.push_context_set ~strict:true ctx
-
-(** Declaration of constants and parameters *)
-
-type constant_obj = {
-  cst_kind : Decls.logical_kind;
-  cst_locl : import_status;
-}
-
-type 'a proof_entry = {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Id.Set.t 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;
-}
-
-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 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 *)
-let load_constant i ((sp,kn), obj) =
-  if Nametab.exists_cci sp then
-    raise (AlreadyDeclared (None, Libnames.basename sp));
-  let con = Global.constant_of_delta_kn kn in
-  Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con);
-  Dumpglob.add_constant_kind con obj.cst_kind
-
-(* Opening means making the name without its module qualification available *)
-let open_constant f i ((sp,kn), obj) =
-  (* Never open a local definition *)
-  match obj.cst_locl with
-  | ImportNeedQualified -> ()
-  | ImportDefaultBehavior ->
-    let con = Global.constant_of_delta_kn kn in
-    if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
-      Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
-
-let exists_name id =
-  Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
-
-let check_exists id =
-  if exists_name id then
-    raise (AlreadyDeclared (None, id))
-
-let cache_constant ((sp,kn), obj) =
-  (* Invariant: the constant must exist in the logical environment, except when
-     redefining it when exiting a section. See [discharge_constant]. *)
-  let kn' =
-    if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
-    then Constant.make1 kn
-    else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
-  in
-  assert (Constant.equal kn' (Constant.make1 kn));
-  Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
-  Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
-
-let discharge_constant ((sp, kn), obj) =
-  Some obj
-
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant cst = {
-  cst_kind = cst.cst_kind;
-  cst_locl = cst.cst_locl;
-}
-
-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;
-    open_function = open_constant;
-    classify_function = classify_constant;
-    subst_function = ident_subst_function;
-    discharge_function = discharge_constant }
-
-let inConstant v = Libobject.Dyn.Easy.inj v objConstant
-
-let update_tables c =
-  Impargs.declare_constant_implicits c;
-  Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
-
-let register_constant kn kind local =
-  let o = inConstant {
-    cst_kind = kind;
-    cst_locl = local;
-  } in
-  let id = Label.to_id (Constant.label kn) in
-  let _ = Lib.add_leaf id o in
-  update_tables kn
-
-let register_side_effect (c, role) =
-  let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
-  match role with
-  | None -> ()
-  | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
-
-let get_roles export eff =
-  let map c =
-    let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
-    (c, role)
-  in
-  List.map map export
-
-let export_side_effects eff =
-  let export = Global.export_private_constants eff.Evd.seff_private in
-  let export = get_roles export eff in
-  List.iter register_side_effect export
-
-let record_aux env s_ty s_bo =
-  let open Environ in
-  let in_ty = keep_hyps env s_ty in
-  let v =
-    String.concat " "
-      (CList.map_filter (fun decl ->
-          let id = NamedDecl.get_id decl in
-          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
-          else Some (Id.to_string id))
-        (keep_hyps env s_bo)) in
-  Aux_file.record_in_aux "context_used" v
-
-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), ());
-    proof_entry_secctx = None;
-    proof_entry_type = types;
-    proof_entry_universes = univs;
-    proof_entry_opaque = opaque;
-    proof_entry_feedback = None;
-    proof_entry_inline_code = inline}
-
-let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
-  { proof_entry_body = body
-  ; 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 = false
-  }
-
-let cast_proof_entry e =
-  let (body, ctx), () = Future.force e.proof_entry_body in
-  let univs =
-    if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
-    else match e.proof_entry_universes with
-      | Entries.Monomorphic_entry ctx' ->
-        (* This can actually happen, try compiling EqdepFacts for instance *)
-        Entries.Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
-      | Entries.Polymorphic_entry _ ->
-        CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
-  in
-  { 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;
-    const_entry_universes = univs;
-    const_entry_inline_code = e.proof_entry_inline_code;
-  }
-
-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 Entries.opaque_entry =
-  let typ = match e.proof_entry_type with
-  | None -> assert false
-  | Some typ -> typ
-  in
-  let secctx = match e.proof_entry_secctx with
-  | None ->
-    let open Environ in
-    let env = Global.env () in
-    let hyp_typ, hyp_def =
-      if List.is_empty (Environ.named_context env) then
-        Id.Set.empty, Id.Set.empty
-      else
-        let ids_typ = global_vars_set env typ in
-        let pf, env = match entry with
-        | PureEntry ->
-          let (pf, _), () = Future.force e.proof_entry_body in
-          pf, env
-        | EffectEntry ->
-          let (pf, _), eff = Future.force e.proof_entry_body in
-          let env = Safe_typing.push_private_constants env eff in
-          pf, env
-        in
-        let vars = global_vars_set env pf in
-        ids_typ, vars
-    in
-    let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
-    Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
-  | Some hyps -> hyps
-  in
-  let (body, univs : b * _) = match entry with
-  | PureEntry ->
-    let (body, uctx), () = Future.force e.proof_entry_body in
-    let univs = match e.proof_entry_universes with
-    | 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
-  { Entries.opaque_entry_body = body;
-    opaque_entry_secctx = secctx;
-    opaque_entry_feedback = e.proof_entry_feedback;
-    opaque_entry_type = typ;
-    opaque_entry_universes = univs;
-  }
-
-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)
-
-let define_constant ~name cd =
-  (* Logically define the constant and its subproofs, no libobject tampering *)
-  let decl, unsafe = match cd with
-    | DefinitionEntry de ->
-      (* We deal with side effects *)
-      if not de.proof_entry_opaque then
-        let body, eff = Future.force de.proof_entry_body in
-        (* This globally defines the side-effects in the environment
-           and registers their libobjects. *)
-        let () = export_side_effects eff in
-        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
-        let cd = Entries.DefinitionEntry (cast_proof_entry de) in
-        ConstantEntry cd, false
-      else
-        let map (body, eff) = body, eff.Evd.seff_private in
-        let body = Future.chain de.proof_entry_body map in
-        let de = { de with proof_entry_body = body } in
-        let de = cast_opaque_proof_entry EffectEntry de in
-        OpaqueEntry de, false
-    | ParameterEntry e ->
-      ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
-    | PrimitiveEntry e ->
-      ConstantEntry (Entries.PrimitiveEntry e), false
-  in
-  let kn = Global.add_constant name decl in
-  if unsafe || is_unsafe_typing_flags() then feedback_axiom();
-  kn
-
-let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
-  let () = check_exists name in
-  let kn = define_constant ~name cd in
-  (* Register the libobjects attached to the constants *)
-  let () = register_constant kn kind local in
-  kn
-
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
-  let kn, eff =
-    let de =
-      if not de.proof_entry_opaque then
-        DefinitionEff (cast_proof_entry de)
-      else
-        let de = cast_opaque_proof_entry PureEntry de in
-        OpaqueEff de
-    in
-    Global.add_private_constant name de
-  in
-  let () = register_constant kn kind local in
-  let seff_roles = match role with
-  | None -> Cmap.empty
-  | Some r -> Cmap.singleton kn r
-  in
-  let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
-  kn, eff
-
-let inline_private_constants ~uctx env ce =
-  let body, eff = Future.force ce.proof_entry_body in
-  let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
-  let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
-  cb, uctx
-
-(** Declaration of section variables and local definitions *)
-type variable_declaration =
-  | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
-
-(* 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)}
-
-let inVariable v = Libobject.Dyn.Easy.inj v objVariable
-
-let declare_variable ~name ~kind d =
-  (* Variables are distinguished by only short names *)
-  if Decls.variable_exists name then
-    raise (AlreadyDeclared (None, name));
-
-  let impl,opaque = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum {typ;impl} ->
-      let () = Global.push_named_assum (name,typ) in
-      impl, true
-    | 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 ((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
-        | 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 = {
-        Entries.secdef_body = body;
-        secdef_secctx = de.proof_entry_secctx;
-        secdef_feedback = de.proof_entry_feedback;
-        secdef_type = de.proof_entry_type;
-      } in
-      let () = Global.push_named_def (name, se) in
-      Glob_term.Explicit, de.proof_entry_opaque
-  in
-  Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  Decls.(add_variable_data name {opaque;kind});
-  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)
-
-(* Declaration messages *)
-
-let pr_rank i = pr_nth (i+1)
-
-let fixpoint_message indexes l =
-  Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> CErrors.anomaly (Pp.str "no recursive definition.")
-  | [id] -> Id.print id ++ str " is recursively defined" ++
-      (match indexes with
-         | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
-         | _ -> mt ())
-  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
-                  spc () ++ str "are recursively defined" ++
-                  match indexes with
-                    | Some a -> spc () ++ str "(decreasing respectively on " ++
-                        prvect_with_sep pr_comma pr_rank a ++
-                        str " arguments)"
-                    | None -> mt ()))
-
-let cofixpoint_message l =
-  Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> CErrors.anomaly (Pp.str "No corecursive definition.")
-  | [id] -> Id.print id ++ str " is corecursively defined"
-  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
-                    spc () ++ str "are corecursively defined"))
-
-let recursive_message isfix i l =
-  (if isfix then fixpoint_message i else cofixpoint_message) l
-
-let definition_message id =
-  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
-
-let assumption_message id =
-  (* Changing "assumed" to "declared", "assuming" referring more to
-  the type of the object than to the name of the object (see
-  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
-  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
-
-module Internal = struct
-
-  let map_entry_body ~f entry =
-    { entry with proof_entry_body = Future.chain entry.proof_entry_body f }
-
-  let map_entry_type ~f entry =
-    { entry with proof_entry_type = f entry.proof_entry_type }
-
-  let set_opacity ~opaque entry =
-    { entry with proof_entry_opaque = opaque }
-
-  let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body
-
-  let rec decompose len c t accu =
-    let open Constr in
-    let open Context.Rel.Declaration in
-    if len = 0 then (c, t, accu)
-    else match kind c, kind t with
-      | Lambda (na, u, c), Prod (_, _, t) ->
-        decompose (pred len) c t (LocalAssum (na, u) :: accu)
-      | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
-        decompose (pred len) c t (LocalDef (na, b, u) :: accu)
-      | _ -> assert false
-
-  let rec shrink ctx sign c t accu =
-    let open Constr in
-    let open Vars in
-    match ctx, sign with
-    | [], [] -> (c, t, accu)
-    | p :: ctx, decl :: sign ->
-      if noccurn 1 c && noccurn 1 t then
-        let c = subst1 mkProp c in
-        let t = subst1 mkProp t in
-        shrink ctx sign c t accu
-      else
-        let c = Term.mkLambda_or_LetIn p c in
-        let t = Term.mkProd_or_LetIn p t in
-        let accu = if Context.Rel.Declaration.is_local_assum p
-          then mkVar (NamedDecl.get_id decl) :: accu
-          else accu
-        in
-        shrink ctx sign c t accu
-    | _ -> assert false
-
-  let shrink_entry sign const =
-    let typ = match const.proof_entry_type with
-      | None -> assert false
-      | Some t -> t
-    in
-    (* The body has been forced by the call to [build_constant_by_tactic] *)
-    let () = assert (Future.is_over const.proof_entry_body) in
-    let ((body, uctx), eff) = Future.force const.proof_entry_body in
-    let (body, typ, ctx) = decompose (List.length sign) body typ [] in
-    let (body, typ, args) = shrink ctx sign body typ [] in
-    { const with
-      proof_entry_body = Future.from_val ((body, uctx), eff)
-    ; proof_entry_type = Some typ
-    }, args
-
-  type nonrec constant_obj = constant_obj
-
-  let objVariable = objVariable
-  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 (Proof.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
-
-let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
-  (* EJGA: flush_and_check_evars is only used in abstract, could we
-     use a different API? *)
-  let concl =
-    try Evarutil.flush_and_check_evars sigma concl
-    with Evarutil.Uninstantiated_evar _ ->
-      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
-  in
-  let sigma, concl =
-    (* FIXME: should be done only if the tactic succeeds *)
-    let sigma = Evd.minimize_universes sigma in
-    sigma, Evarutil.nf_evars_universes sigma concl
-  in
-  let concl = EConstr.of_constr concl in
-  let uctx = Evd.evar_universe_context sigma in
-  let (const, safe, uctx) =
-    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~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
-       means that [e] comes from [tac] failing to yield enough
-       success). Hence it reraises [e]. *)
-    let (_, info) = Exninfo.capture src in
-    Exninfo.iraise (e, info)
-  in
-  let sigma = Evd.set_universe_context sigma uctx in
-  let body, effs = Future.force const.proof_entry_body in
-  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
-  let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
-  (* 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`
-     kernel will boom. This deserves more investigation. *)
-  let const = Internal.set_opacity ~opaque const in
-  let const, args = Internal.shrink_entry sign const in
-  let cst () =
-    (* do not compute the implicit arguments, it may be costly *)
-    let () = Impargs.make_implicit_args false in
-    (* ppedrot: seems legit to have abstracted subproofs as local*)
-    declare_private_constant ~local:ImportNeedQualified ~name ~kind const
-  in
-  let cst, eff = Impargs.with_implicit_protection cst () in
-  let inst = match const.proof_entry_universes with
-  | Entries.Monomorphic_entry _ -> EConstr.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_entry_body in
-    let () = assert (Univ.ContextSet.is_empty body_uctx) in
-    EConstr.EInstance.make (Univ.UContext.instance ctx)
-  in
-  let args = List.map EConstr.of_constr args in
-  let lem = EConstr.mkConstU (cst, inst) in
-  let effs = Evd.concat_side_effects eff effs in
-  effs, sigma, lem, args, safe
-
-let get_goal_context pf i =
-  let p = get_proof pf in
-  Proof.get_goal_context_gen p i
-
-let get_current_goal_context pf =
-  let p = get_proof pf in
-  try Proof.get_goal_context_gen p 1
-  with
-  | Proof.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 = get_proof pf in
-  Proof.get_proof_context p
-
-module Proof = struct
-  type nonrec t = t
-  let get_proof = get_proof
-  let get_proof_name = get_proof_name
-  let get_used_variables = get_used_variables
-  let get_universe_decl = get_universe_decl
-  let get_initial_euctx = get_initial_euctx
-  let map_proof = map_proof
-  let map_fold_proof = map_fold_proof
-  let map_fold_proof_endline = map_fold_proof_endline
-  let set_endline_tactic = set_endline_tactic
-  let set_used_variables = set_used_variables
-  let compact = compact_the_proof
-  let update_global_env = update_global_env
-  let get_open_goals = get_open_goals
-end
diff --git a/tactics/declare.mli b/tactics/declare.mli
deleted file mode 100644
index 1fabf80b2a..0000000000
--- a/tactics/declare.mli
+++ /dev/null
@@ -1,314 +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 Names
-open Constr
-open 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.Proof.t] Construction of constants using interactive proofs. *)
-module Proof : sig
-
-  type t
-
-  (** XXX: These are internal and will go away from publis API once
-     lemmas is merged here *)
-  val get_proof : t -> Proof.t
-  val get_proof_name : t -> Names.Id.t
-
-  (** XXX: These 3 are only used in lemmas  *)
-  val get_used_variables : t -> Names.Id.Set.t option
-  val get_universe_decl : t -> UState.universe_decl
-  val get_initial_euctx : t -> UState.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
-
-  val compact : t -> 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
-
-  val get_open_goals : t -> int
-
-end
-
-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
-  -> Proof.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
-  -> Proof.t
-
-(** Proof entries represent a proof that has been finished, but still
-   not registered with the kernel.
-
-   XXX: Scheduled for removal from public API, don't rely on it *)
-type 'a proof_entry = private {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Id.Set.t 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;
-}
-
-(** XXX: Scheduled for removal from public API, don't rely on it *)
-type proof_object = private
-  { 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 -> Proof.t -> proof_object
-
-(** Declaration of local constructions (Variable/Hypothesis/Local) *)
-
-(** XXX: Scheduled for removal from public API, don't rely on it *)
-type variable_declaration =
-  | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
-
-(** XXX: Scheduled for removal from public API, don't rely on it *)
-type 'a constant_entry =
-  | DefinitionEntry of 'a proof_entry
-  | ParameterEntry of parameter_entry
-  | PrimitiveEntry of primitive_entry
-
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
-val declare_variable
-  :  name:variable
-  -> kind:Decls.logical_kind
-  -> variable_declaration
-  -> unit
-
-(** Declaration of global constructions
-   i.e. Definition/Theorem/Axiom/Parameter/...
-
-   XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
-val definition_entry
-  : ?fix_exn:Future.fix_exn
-  -> ?opaque:bool
-  -> ?inline:bool
-  -> ?feedback_id:Stateid.t
-  -> ?section_vars:Id.Set.t
-  -> ?types:types
-  -> ?univs:Entries.universes_entry
-  -> ?eff:Evd.side_effects
-  -> ?univsbody:Univ.ContextSet.t
-  (** Universe-constraints attached to the body-only, used in
-     vio-delayed opaque constants and private poly universes *)
-  -> constr
-  -> Evd.side_effects proof_entry
-
-(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
-val pure_definition_entry
-  : ?fix_exn:Future.fix_exn
-  -> ?opaque:bool
-  -> ?inline:bool
-  -> ?types:types
-  -> ?univs:Entries.universes_entry
-  -> constr
-  -> unit proof_entry
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-(** [declare_constant id cd] declares a global declaration
-   (constant/parameter) with name [id] in the current section; it returns
-   the full path of the declaration
-
-  internal specify if the constant has been created by the kernel or by the
-  user, and in the former case, if its errors should be silent
-
-  XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
-val declare_constant
-  :  ?local:import_status
-  -> name:Id.t
-  -> kind:Decls.logical_kind
-  -> Evd.side_effects constant_entry
-  -> Constant.t
-
-val declare_private_constant
-  :  ?role:Evd.side_effect_role
-  -> ?local:import_status
-  -> name:Id.t
-  -> kind:Decls.logical_kind
-  -> unit proof_entry
-  -> Constant.t * Evd.side_effects
-
-(** [inline_private_constants ~sideff ~uctx env ce] will inline the
-   constants in [ce]'s body and return the body plus the updated
-   [UState.t].
-
-   XXX: Scheduled for removal from public API, don't rely on it *)
-val inline_private_constants
-  :  uctx:UState.t
-  -> Environ.env
-  -> Evd.side_effects proof_entry
-  -> Constr.t * UState.t
-
-(** Declaration messages *)
-
-(** XXX: Scheduled for removal from public API, do not use *)
-val definition_message : Id.t -> unit
-val assumption_message : Id.t -> unit
-val fixpoint_message : int array option -> Id.t list -> unit
-val recursive_message : bool (** true = fixpoint *) ->
-  int array option -> Id.t list -> unit
-
-val check_exists : Id.t -> unit
-
-(* Used outside this module only in indschemes *)
-exception AlreadyDeclared of (string option * Id.t)
-
-(** {6 For legacy support, do not use}  *)
-
-module Internal : sig
-
-  val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
-  val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
-  (* Overriding opacity is indeed really hacky *)
-  val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
-
-  (* TODO: This is only used in DeclareDef to forward the fix to
-     hooks, should eventually go away *)
-  val get_fix_exn : 'a proof_entry -> Future.fix_exn
-
-  val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
-
-  type constant_obj
-
-  val objConstant : constant_obj Libobject.Dyn.tag
-  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 : 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 : Proof.t -> closed_proof_output
-val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
-
-(** [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.t -> Proof.t * bool
-
-(** Declare abstract constant; will check no evars are possible; *)
-val declare_abstract :
-     name:Names.Id.t
-  -> poly:bool
-  -> kind:Decls.logical_kind
-  -> sign:EConstr.named_context
-  -> secsign:Environ.named_context_val
-  -> opaque:bool
-  -> solve_tac:unit Proofview.tactic
-  -> Evd.evar_map
-  -> EConstr.t
-  -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool
-
-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 Helpers to obtain proof state when in an interactive proof } *)
-
-(** [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.t -> int -> Evd.evar_map * Environ.env
-
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_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 : Proof.t -> Evd.evar_map * Environ.env
-
-(** Temporarily re-exported for 3rd party code; don't use  *)
-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
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
new file mode 100644
index 0000000000..3f67ff20a4
--- /dev/null
+++ b/tactics/declareUctx.ml
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** Monomorphic universes need to survive sections. *)
+
+let name_instance inst =
+  let map lvl = match Univ.Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        Names.Name (Libnames.qualid_basename qid)
+      with Not_found ->
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
+        Names.Name (Names.Id.of_string_soft (Univ.Level.to_string lvl))
+  in
+  Array.map map (Univ.Instance.to_array inst)
+
+let declare_universe_context ~poly ctx =
+  if poly then
+    let uctx = Univ.ContextSet.to_context ctx in
+    let nas = name_instance (Univ.UContext.instance uctx) in
+    Global.push_section_context (nas, uctx)
+  else
+    Global.push_context_set ~strict:true ctx
diff --git a/tactics/declareUctx.mli b/tactics/declareUctx.mli
new file mode 100644
index 0000000000..7ecfab04f2
--- /dev/null
+++ b/tactics/declareUctx.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0499ba200e..5fb519cc4f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -878,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr =
     else begin
       if isgr then
         warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
-      Declare.declare_universe_context ~poly:false ctx;
+      DeclareUctx.declare_universe_context ~poly:false ctx;
       (c, Univ.ContextSet.empty)
     end
 
@@ -1437,8 +1437,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 = Declare.Proof.get_proof pf in
-  let Proof.{goals;sigma} = Proof.data pts in
+  let Proof.{goals;sigma} = Proof.data pf in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index a54da8ef0a..f5fd3348e4 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -288,7 +288,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Declare.Proof.t -> Pp.t
+val pr_applicable_hint : Proof.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/ind_tables.ml b/tactics/ind_tables.ml
index 8336fae02f..e422366ed6 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -86,15 +86,15 @@ let compute_name internal id =
     Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
   else id
 
+let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
+    CErrors.anomaly (Pp.str "scheme declaration not registered"))
+
 let define internal role id c poly univs =
   let id = compute_name internal id in
   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 = Declare.pure_definition_entry ~univs c in
-  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
-  let () = if internal then () else Declare.definition_message id in
-  kn, eff
+  !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let (c, ctx), eff = f mode ind in
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index dad2036c64..736de2af37 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -59,3 +59,11 @@ val check_scheme : 'a scheme_kind -> inductive -> bool
 val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
 
 val pr_scheme_kind : 'a scheme_kind -> Pp.t
+
+val declare_definition_scheme :
+  (internal : bool
+   -> univs:Entries.universes_entry
+   -> role:Evd.side_effect_role
+   -> name:Id.t
+   -> Constr.t
+   -> Constant.t * Evd.side_effects) ref
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
deleted file mode 100644
index 5a8ec404ee..0000000000
--- a/tactics/leminv.ml
+++ /dev/null
@@ -1,297 +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 Pp
-open CErrors
-open Util
-open Names
-open Termops
-open Environ
-open Constr
-open Context
-open EConstr
-open Vars
-open Namegen
-open Evd
-open Printer
-open Reductionops
-open Inductiveops
-open Tacmach.New
-open Clenv
-open Tacticals.New
-open Tactics
-open Context.Named.Declaration
-
-module NamedDecl = Context.Named.Declaration
-
-let no_inductive_inconstr env sigma constr =
-  (str "Cannot recognize an inductive predicate in " ++
-     pr_leconstr_env env sigma constr ++
-     str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
-     spc () ++ str "or of the type of constructors" ++ spc () ++
-     str "is hidden by constant definitions.")
-
-(* Inversion stored in lemmas *)
-
-(* ALGORITHM:
-
-   An inversion stored in a lemma is computed from a term-pattern, in
-   a signature, as follows:
-
-   Suppose we have an inductive relation, (I abar), in a signature Gamma:
-
-       Gamma |- (I abar)
-
-   Then we compute the free-variables of abar.  Suppose that Gamma is
-   thinned out to only include these.
-
-   [We need technically to require that all free-variables of the
-    types of the free variables of abar are themselves free-variables
-    of abar.  This needs to be checked, but it should not pose a
-    problem - it is hard to imagine cases where it would not hold.]
-
-   Now, we pose the goal:
-
-       (P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]).
-
-   We execute the tactic:
-
-   REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME))
-
-   This leaves us with some subgoals.  All the assumptions after "P"
-   in these subgoals are new assumptions.  I.e. if we have a subgoal,
-
-       P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar)
-
-   then the assumption we needed to have was
-
-      (Hbar:Tbar)(P ybar)
-
-   So we construct all the assumptions we need, and rebuild the goal
-   with these assumptions.  Then, we can re-apply the same tactic as
-   above, but instead of stopping after the inversion, we just apply
-   the respective assumption in each subgoal.
-
- *)
-
-(* returns the sub_signature of sign corresponding to those identifiers that
- * are not global. *)
-(*
-let get_local_sign sign =
-  let lid = ids_of_sign sign in
-  let globsign = Global.named_context() in
-  let add_local id res_sign =
-    if not (mem_sign globsign id) then
-      add_sign (lookup_sign id sign) res_sign
-    else
-      res_sign
-  in
-  List.fold_right add_local lid nil_sign
-*)
-(* returns the identifier of lid that was the latest declared in sign.
- * (i.e. is the identifier id of lid such that
- * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
- * for any id'<>id in lid).
- * it returns both the pair (id,(sign_prefix id sign)) *)
-(*
-let max_prefix_sign lid sign =
-  let rec max_rec (resid,prefix) = function
-    | [] -> (resid,prefix)
-    | (id::l) ->
-        let pre = sign_prefix id sign in
-        if sign_length pre > sign_length prefix then
-          max_rec (id,pre) l
-        else
-          max_rec (resid,prefix) l
-  in
-  match lid with
-    | [] -> nil_sign
-    | id::l -> snd (max_rec (id, sign_prefix id sign) l)
-*)
-let rec add_prods_sign env sigma t =
-  match EConstr.kind sigma (whd_all env sigma t) with
-    | Prod (na,c1,b) ->
-        let id = id_of_name_using_hdchar env sigma t na.binder_name in
-        let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
-    | LetIn (na,c1,t1,b) ->
-        let id = id_of_name_using_hdchar env sigma t na.binder_name in
-        let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
-    | _ -> (env,t)
-
-(* [dep_option] indicates whether the inversion lemma is dependent or not.
-   If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
-   the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
-   where P:(x_bar:T_bar)(H:(I x_bar))[sort].
-   The generalisation of such a goal at the moment of the dependent case should
-   be easy.
-
-   If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the
-   variables occurring in [I], then the stated goal will be:
-    (x_bar:T_bar)(I t_bar)->(P x_bar)
-   where P: P:(x_bar:T_bar)[sort].
-*)
-
-let compute_first_inversion_scheme env sigma ind sort dep_option =
-  let indf,realargs = dest_ind_type ind in
-  let allvars = vars_of_env env in
-  let p = next_ident_away (Id.of_string "P") allvars in
-  let pty,goal =
-    if dep_option  then
-      let pty = make_arity env sigma true indf sort in
-      let r = relevance_of_inductive_type env ind in
-      let goal =
-        mkProd
-          (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
-      in
-      pty,goal
-    else
-      let i = mkAppliedInd ind in
-      let ivars = global_vars env sigma i in
-      let revargs,ownsign =
-        fold_named_context
-          (fun env d (revargs,hyps) ->
-            let d = map_named_decl EConstr.of_constr d in
-             let id = NamedDecl.get_id d in
-             if Id.List.mem id ivars then
-               ((mkVar id)::revargs, Context.Named.add d hyps)
-             else
-               (revargs,hyps))
-          env ~init:([],[])
-      in
-      let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
-      let goal = mkArrow i Sorts.Relevant (applist(mkVar p, List.rev revargs)) in
-      (pty,goal)
-  in
-  let npty = nf_all env sigma pty in
-  let extenv = push_named (LocalAssum (make_annot p Sorts.Relevant,npty)) env in
-  extenv, goal
-
-(* [inversion_scheme sign I]
-
-   Given a local signature, [sign], and an instance of an inductive
-   relation, [I], inversion_scheme will prove the associated inversion
-   scheme on sort [sort]. Depending on the value of [dep_option] it will
-   build a dependent lemma or a non-dependent one *)
-
-let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
-  let (env,i) = add_prods_sign env sigma t in
-  let ind =
-    try find_rectype env sigma i
-    with Not_found ->
-      user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
-  in
-  let (invEnv,invGoal) =
-    compute_first_inversion_scheme env sigma ind sort dep_option
-  in
-  assert
-    (List.subset
-       (global_vars env sigma invGoal)
-       (ids_of_named_context (named_context invEnv)));
-  (*
-    user_err ~hdr:"lemma_inversion"
-    (str"Computed inversion goal was not closed in initial signature.");
-  *)
-  let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
-  let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
-  let pfterm = List.hd (Proof.partial_proof pf) in
-  let global_named_context = Global.named_context_val () in
-  let ownSign = ref begin
-    fold_named_context
-      (fun env d sign ->
-        let d = map_named_decl EConstr.of_constr d in
-         if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
-         else Context.Named.add d sign)
-      invEnv ~init:Context.Named.empty
-  end in
-  let avoid = ref Id.Set.empty in
-  let Proof.{sigma} = Proof.data pf in
-  let sigma = Evd.minimize_universes sigma in
-  let rec fill_holes c =
-    match EConstr.kind sigma c with
-    | Evar (e,args) ->
-        let h = next_ident_away (Id.of_string "H") !avoid in
-        let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
-        avoid := Id.Set.add h !avoid;
-        ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
-        applist (mkVar h, inst)
-    | _ -> EConstr.map sigma fill_holes c
-  in
-  let c = fill_holes pfterm in
-  (* warning: side-effect on ownSign *)
-  let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
-  let p = EConstr.to_constr sigma invProof in
-  p, sigma
-
-let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
-  let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
-  let univs = Evd.univ_entry ~poly sigma in
-  let entry = Declare.definition_entry ~univs invProof in
-  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
-  ()
-
-(* inv_op = Inv (derives de complete inv. lemma)
- * inv_op = InvNoThining (derives de semi inversion lemma) *)
-
-let add_inversion_lemma_exn ~poly na com comsort bool tac =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
-  let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
-  try
-    add_inversion_lemma ~poly na env sigma c sort bool tac
-  with
-    |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
-          user_err ~hdr:"Inv needs Nodep Prop Set" s
-
-(* ================================= *)
-(* Applying a given inversion lemma  *)
-(* ================================= *)
-
-let lemInv id c =
-  Proofview.Goal.enter begin fun gls ->
-  try
-    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
-    let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
-    Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
-  with
-    | NoSuchBinding ->
-        user_err
-          (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
-    | UserError (a,b) ->
-         user_err ~hdr:"LemInv"
-           (str "Cannot refine current goal with the lemma " ++
-              pr_leconstr_env (pf_env gls) (project gls) c)
-  end
-
-let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
-
-let lemInvIn id c ids =
-  Proofview.Goal.enter begin fun gl ->
-    let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
-    let intros_replace_ids =
-      let concl = Proofview.Goal.concl gl in
-      let sigma = project gl in
-      let nb_of_new_hyp = nb_prod sigma concl - List.length ids in
-      if nb_of_new_hyp < 1  then
-        intros_replacing ids
-      else
-        (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
-    in
-    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
-        (intros_replace_ids)))
-  end
-
-let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
-
-let lemInv_clause id c = function
-  | [] -> lemInv_gen id c
-  | l -> lemInvIn_gen id c l
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
deleted file mode 100644
index 5a5de7b58f..0000000000
--- a/tactics/leminv.mli
+++ /dev/null
@@ -1,21 +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 Names
-open EConstr
-open Constrexpr
-open Tactypes
-
-val lemInv_clause :
-  quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
-
-val add_inversion_lemma_exn : poly:bool ->
-  Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
-    unit
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 537d111f23..36d61feed1 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,4 @@
 DeclareScheme
-Declare
 Dnet
 Dn
 Btermdn
@@ -18,7 +17,7 @@ Elim
 Equality
 Contradiction
 Inv
-Leminv
+DeclareUctx
 Hints
 Auto
 Eauto
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 43e86fa9bd..776ffd6b9f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -91,7 +91,7 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
   let () = match scope with
     | Discharge ->
       (* declare universes separately for variables *)
-      Declare.declare_universe_context ~poly (context_set_of_entry (fst univs))
+      DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
     | Global _ -> ()
   in
   let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
@@ -191,7 +191,7 @@ let context_subst subst (name,b,t,impl) =
 
 let context_insection sigma ~poly ctx =
   let uctx = Evd.universe_context_set sigma in
-  let () = Declare.declare_universe_context ~poly uctx in
+  let () = DeclareUctx.declare_universe_context ~poly uctx in
   let fn subst (name,_,_,_ as d) =
     let d = context_subst subst d in
     let () = match d with
@@ -226,7 +226,7 @@ let context_nosection sigma ~poly ctx =
       (* Multiple monomorphic axioms: declare universes separately to
          avoid redeclaring them. *)
       let uctx = Evd.universe_context_set sigma in
-      let () = Declare.declare_universe_context ~poly uctx in
+      let () = DeclareUctx.declare_universe_context ~poly uctx in
       Monomorphic_entry Univ.ContextSet.empty
   in
   let fn subst d =
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 324fee72ec..5a48e9c16c 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -97,7 +97,7 @@ let interp_hints ~poly h =
     let c, diff = Hints.prepare_hint true env sigma (evd, c) in
     if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
     else
-      let () = Declare.declare_universe_context ~poly:false diff in
+      let () = DeclareUctx.declare_universe_context ~poly:false diff in
       (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
   in
   let fref r =
diff --git a/vernac/declare.ml b/vernac/declare.ml
new file mode 100644
index 0000000000..6a4511ead8
--- /dev/null
+++ b/vernac/declare.ml
@@ -0,0 +1,886 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** This module is about the low-level declaration of logical objects *)
+
+open Pp
+open Util
+open Names
+open Safe_typing
+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)
+
+let _ = CErrors.register_handler (function
+    | AlreadyDeclared (kind, id) ->
+      Some
+        (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
+             ; Id.print id; str " already exists."])
+    | _ ->
+      None)
+
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
+(** Declaration of constants and parameters *)
+
+type constant_obj = {
+  cst_kind : Decls.logical_kind;
+  cst_locl : import_status;
+}
+
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Id.Set.t 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;
+}
+
+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 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 *)
+let load_constant i ((sp,kn), obj) =
+  if Nametab.exists_cci sp then
+    raise (AlreadyDeclared (None, Libnames.basename sp));
+  let con = Global.constant_of_delta_kn kn in
+  Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con);
+  Dumpglob.add_constant_kind con obj.cst_kind
+
+(* Opening means making the name without its module qualification available *)
+let open_constant f i ((sp,kn), obj) =
+  (* Never open a local definition *)
+  match obj.cst_locl with
+  | ImportNeedQualified -> ()
+  | ImportDefaultBehavior ->
+    let con = Global.constant_of_delta_kn kn in
+    if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
+      Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
+
+let exists_name id =
+  Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
+
+let check_exists id =
+  if exists_name id then
+    raise (AlreadyDeclared (None, id))
+
+let cache_constant ((sp,kn), obj) =
+  (* Invariant: the constant must exist in the logical environment, except when
+     redefining it when exiting a section. See [discharge_constant]. *)
+  let kn' =
+    if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
+    then Constant.make1 kn
+    else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
+  in
+  assert (Constant.equal kn' (Constant.make1 kn));
+  Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
+  Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
+
+let discharge_constant ((sp, kn), obj) =
+  Some obj
+
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_constant cst = {
+  cst_kind = cst.cst_kind;
+  cst_locl = cst.cst_locl;
+}
+
+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;
+    open_function = open_constant;
+    classify_function = classify_constant;
+    subst_function = ident_subst_function;
+    discharge_function = discharge_constant }
+
+let inConstant v = Libobject.Dyn.Easy.inj v objConstant
+
+let update_tables c =
+  Impargs.declare_constant_implicits c;
+  Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
+
+let register_constant kn kind local =
+  let o = inConstant {
+    cst_kind = kind;
+    cst_locl = local;
+  } in
+  let id = Label.to_id (Constant.label kn) in
+  let _ = Lib.add_leaf id o in
+  update_tables kn
+
+let register_side_effect (c, role) =
+  let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
+  match role with
+  | None -> ()
+  | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
+
+let get_roles export eff =
+  let map c =
+    let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+    (c, role)
+  in
+  List.map map export
+
+let export_side_effects eff =
+  let export = Global.export_private_constants eff.Evd.seff_private in
+  let export = get_roles export eff in
+  List.iter register_side_effect export
+
+let record_aux env s_ty s_bo =
+  let open Environ in
+  let in_ty = keep_hyps env s_ty in
+  let v =
+    String.concat " "
+      (CList.map_filter (fun decl ->
+          let id = NamedDecl.get_id decl in
+          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" v
+
+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), ());
+    proof_entry_secctx = None;
+    proof_entry_type = types;
+    proof_entry_universes = univs;
+    proof_entry_opaque = opaque;
+    proof_entry_feedback = None;
+    proof_entry_inline_code = inline}
+
+let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
+  { proof_entry_body = body
+  ; 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 = false
+  }
+
+let cast_proof_entry e =
+  let (body, ctx), () = Future.force e.proof_entry_body in
+  let univs =
+    if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
+    else match e.proof_entry_universes with
+      | Entries.Monomorphic_entry ctx' ->
+        (* This can actually happen, try compiling EqdepFacts for instance *)
+        Entries.Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
+      | Entries.Polymorphic_entry _ ->
+        CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
+  in
+  { 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;
+    const_entry_universes = univs;
+    const_entry_inline_code = e.proof_entry_inline_code;
+  }
+
+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 Entries.opaque_entry =
+  let typ = match e.proof_entry_type with
+  | None -> assert false
+  | Some typ -> typ
+  in
+  let secctx = match e.proof_entry_secctx with
+  | None ->
+    let open Environ in
+    let env = Global.env () in
+    let hyp_typ, hyp_def =
+      if List.is_empty (Environ.named_context env) then
+        Id.Set.empty, Id.Set.empty
+      else
+        let ids_typ = global_vars_set env typ in
+        let pf, env = match entry with
+        | PureEntry ->
+          let (pf, _), () = Future.force e.proof_entry_body in
+          pf, env
+        | EffectEntry ->
+          let (pf, _), eff = Future.force e.proof_entry_body in
+          let env = Safe_typing.push_private_constants env eff in
+          pf, env
+        in
+        let vars = global_vars_set env pf in
+        ids_typ, vars
+    in
+    let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
+    Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
+  | Some hyps -> hyps
+  in
+  let (body, univs : b * _) = match entry with
+  | PureEntry ->
+    let (body, uctx), () = Future.force e.proof_entry_body in
+    let univs = match e.proof_entry_universes with
+    | 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
+  { Entries.opaque_entry_body = body;
+    opaque_entry_secctx = secctx;
+    opaque_entry_feedback = e.proof_entry_feedback;
+    opaque_entry_type = typ;
+    opaque_entry_universes = univs;
+  }
+
+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)
+
+let define_constant ~name cd =
+  (* Logically define the constant and its subproofs, no libobject tampering *)
+  let decl, unsafe = match cd with
+    | DefinitionEntry de ->
+      (* We deal with side effects *)
+      if not de.proof_entry_opaque then
+        let body, eff = Future.force de.proof_entry_body in
+        (* This globally defines the side-effects in the environment
+           and registers their libobjects. *)
+        let () = export_side_effects eff in
+        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+        let cd = Entries.DefinitionEntry (cast_proof_entry de) in
+        ConstantEntry cd, false
+      else
+        let map (body, eff) = body, eff.Evd.seff_private in
+        let body = Future.chain de.proof_entry_body map in
+        let de = { de with proof_entry_body = body } in
+        let de = cast_opaque_proof_entry EffectEntry de in
+        OpaqueEntry de, false
+    | ParameterEntry e ->
+      ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+    | PrimitiveEntry e ->
+      ConstantEntry (Entries.PrimitiveEntry e), false
+  in
+  let kn = Global.add_constant name decl in
+  if unsafe || is_unsafe_typing_flags() then feedback_axiom();
+  kn
+
+let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+  let () = check_exists name in
+  let kn = define_constant ~name cd in
+  (* Register the libobjects attached to the constants *)
+  let () = register_constant kn kind local in
+  kn
+
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
+  let kn, eff =
+    let de =
+      if not de.proof_entry_opaque then
+        DefinitionEff (cast_proof_entry de)
+      else
+        let de = cast_opaque_proof_entry PureEntry de in
+        OpaqueEff de
+    in
+    Global.add_private_constant name de
+  in
+  let () = register_constant kn kind local in
+  let seff_roles = match role with
+  | None -> Cmap.empty
+  | Some r -> Cmap.singleton kn r
+  in
+  let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
+  kn, eff
+
+let inline_private_constants ~uctx env ce =
+  let body, eff = Future.force ce.proof_entry_body in
+  let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
+  let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
+  cb, uctx
+
+(** Declaration of section variables and local definitions *)
+type variable_declaration =
+  | SectionLocalDef of Evd.side_effects proof_entry
+  | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
+
+(* 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)}
+
+let inVariable v = Libobject.Dyn.Easy.inj v objVariable
+
+let declare_variable ~name ~kind d =
+  (* Variables are distinguished by only short names *)
+  if Decls.variable_exists name then
+    raise (AlreadyDeclared (None, name));
+
+  let impl,opaque = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum {typ;impl} ->
+      let () = Global.push_named_assum (name,typ) in
+      impl, true
+    | 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 ((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
+        | 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 () = DeclareUctx.declare_universe_context ~poly univs in
+      let se = {
+        Entries.secdef_body = body;
+        secdef_secctx = de.proof_entry_secctx;
+        secdef_feedback = de.proof_entry_feedback;
+        secdef_type = de.proof_entry_type;
+      } in
+      let () = Global.push_named_def (name, se) in
+      Glob_term.Explicit, de.proof_entry_opaque
+  in
+  Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
+  Decls.(add_variable_data name {opaque;kind});
+  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)
+
+(* Declaration messages *)
+
+let pr_rank i = pr_nth (i+1)
+
+let fixpoint_message indexes l =
+  Flags.if_verbose Feedback.msg_info (match l with
+  | [] -> CErrors.anomaly (Pp.str "no recursive definition.")
+  | [id] -> Id.print id ++ str " is recursively defined" ++
+      (match indexes with
+         | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+         | _ -> mt ())
+  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
+                  spc () ++ str "are recursively defined" ++
+                  match indexes with
+                    | Some a -> spc () ++ str "(decreasing respectively on " ++
+                        prvect_with_sep pr_comma pr_rank a ++
+                        str " arguments)"
+                    | None -> mt ()))
+
+let cofixpoint_message l =
+  Flags.if_verbose Feedback.msg_info (match l with
+  | [] -> CErrors.anomaly (Pp.str "No corecursive definition.")
+  | [id] -> Id.print id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
+                    spc () ++ str "are corecursively defined"))
+
+let recursive_message isfix i l =
+  (if isfix then fixpoint_message i else cofixpoint_message) l
+
+let definition_message id =
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
+
+let assumption_message id =
+  (* Changing "assumed" to "declared", "assuming" referring more to
+  the type of the object than to the name of the object (see
+  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
+
+module Internal = struct
+
+  let map_entry_body ~f entry =
+    { entry with proof_entry_body = Future.chain entry.proof_entry_body f }
+
+  let map_entry_type ~f entry =
+    { entry with proof_entry_type = f entry.proof_entry_type }
+
+  let set_opacity ~opaque entry =
+    { entry with proof_entry_opaque = opaque }
+
+  let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body
+
+  let rec decompose len c t accu =
+    let open Constr in
+    let open Context.Rel.Declaration in
+    if len = 0 then (c, t, accu)
+    else match kind c, kind t with
+      | Lambda (na, u, c), Prod (_, _, t) ->
+        decompose (pred len) c t (LocalAssum (na, u) :: accu)
+      | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
+        decompose (pred len) c t (LocalDef (na, b, u) :: accu)
+      | _ -> assert false
+
+  let rec shrink ctx sign c t accu =
+    let open Constr in
+    let open Vars in
+    match ctx, sign with
+    | [], [] -> (c, t, accu)
+    | p :: ctx, decl :: sign ->
+      if noccurn 1 c && noccurn 1 t then
+        let c = subst1 mkProp c in
+        let t = subst1 mkProp t in
+        shrink ctx sign c t accu
+      else
+        let c = Term.mkLambda_or_LetIn p c in
+        let t = Term.mkProd_or_LetIn p t in
+        let accu = if Context.Rel.Declaration.is_local_assum p
+          then mkVar (NamedDecl.get_id decl) :: accu
+          else accu
+        in
+        shrink ctx sign c t accu
+    | _ -> assert false
+
+  let shrink_entry sign const =
+    let typ = match const.proof_entry_type with
+      | None -> assert false
+      | Some t -> t
+    in
+    (* The body has been forced by the call to [build_constant_by_tactic] *)
+    let () = assert (Future.is_over const.proof_entry_body) in
+    let ((body, uctx), eff) = Future.force const.proof_entry_body in
+    let (body, typ, ctx) = decompose (List.length sign) body typ [] in
+    let (body, typ, args) = shrink ctx sign body typ [] in
+    { const with
+      proof_entry_body = Future.from_val ((body, uctx), eff)
+    ; proof_entry_type = Some typ
+    }, args
+
+  type nonrec constant_obj = constant_obj
+
+  let objVariable = objVariable
+  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 (Proof.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
+
+let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
+  (* EJGA: flush_and_check_evars is only used in abstract, could we
+     use a different API? *)
+  let concl =
+    try Evarutil.flush_and_check_evars sigma concl
+    with Evarutil.Uninstantiated_evar _ ->
+      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
+  in
+  let sigma, concl =
+    (* FIXME: should be done only if the tactic succeeds *)
+    let sigma = Evd.minimize_universes sigma in
+    sigma, Evarutil.nf_evars_universes sigma concl
+  in
+  let concl = EConstr.of_constr concl in
+  let uctx = Evd.evar_universe_context sigma in
+  let (const, safe, uctx) =
+    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~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
+       means that [e] comes from [tac] failing to yield enough
+       success). Hence it reraises [e]. *)
+    let (_, info) = Exninfo.capture src in
+    Exninfo.iraise (e, info)
+  in
+  let sigma = Evd.set_universe_context sigma uctx in
+  let body, effs = Future.force const.proof_entry_body in
+  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
+  let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
+  (* 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`
+     kernel will boom. This deserves more investigation. *)
+  let const = Internal.set_opacity ~opaque const in
+  let const, args = Internal.shrink_entry sign const in
+  let cst () =
+    (* do not compute the implicit arguments, it may be costly *)
+    let () = Impargs.make_implicit_args false in
+    (* ppedrot: seems legit to have abstracted subproofs as local*)
+    declare_private_constant ~local:ImportNeedQualified ~name ~kind const
+  in
+  let cst, eff = Impargs.with_implicit_protection cst () in
+  let inst = match const.proof_entry_universes with
+  | Entries.Monomorphic_entry _ -> EConstr.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_entry_body in
+    let () = assert (Univ.ContextSet.is_empty body_uctx) in
+    EConstr.EInstance.make (Univ.UContext.instance ctx)
+  in
+  let args = List.map EConstr.of_constr args in
+  let lem = EConstr.mkConstU (cst, inst) in
+  let effs = Evd.concat_side_effects eff effs in
+  effs, sigma, lem, args, safe
+
+let get_goal_context pf i =
+  let p = get_proof pf in
+  Proof.get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = get_proof pf in
+  try Proof.get_goal_context_gen p 1
+  with
+  | Proof.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 = get_proof pf in
+  Proof.get_proof_context p
+
+module Proof = struct
+  type nonrec t = t
+  let get_proof = get_proof
+  let get_proof_name = get_proof_name
+  let get_used_variables = get_used_variables
+  let get_universe_decl = get_universe_decl
+  let get_initial_euctx = get_initial_euctx
+  let map_proof = map_proof
+  let map_fold_proof = map_fold_proof
+  let map_fold_proof_endline = map_fold_proof_endline
+  let set_endline_tactic = set_endline_tactic
+  let set_used_variables = set_used_variables
+  let compact = compact_the_proof
+  let update_global_env = update_global_env
+  let get_open_goals = get_open_goals
+end
+
+let declare_definition_scheme ~internal ~univs ~role ~name c =
+  let kind = Decls.(IsDefinition Scheme) in
+  let entry = pure_definition_entry ~univs c in
+  let kn, eff = declare_private_constant ~role ~kind ~name entry in
+  let () = if internal then () else definition_message name in
+  kn, eff
+
+let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
+let _ = Abstract.declare_abstract := declare_abstract
diff --git a/vernac/declare.mli b/vernac/declare.mli
new file mode 100644
index 0000000000..73e0d7cd04
--- /dev/null
+++ b/vernac/declare.mli
@@ -0,0 +1,299 @@
+(************************************************************************)
+(*         *   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 Names
+open Constr
+open 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.Proof.t] Construction of constants using interactive proofs. *)
+module Proof : sig
+
+  type t
+
+  (** XXX: These are internal and will go away from publis API once
+     lemmas is merged here *)
+  val get_proof : t -> Proof.t
+  val get_proof_name : t -> Names.Id.t
+
+  (** XXX: These 3 are only used in lemmas  *)
+  val get_used_variables : t -> Names.Id.Set.t option
+  val get_universe_decl : t -> UState.universe_decl
+  val get_initial_euctx : t -> UState.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
+
+  val compact : t -> 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
+
+  val get_open_goals : t -> int
+
+end
+
+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
+  -> Proof.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
+  -> Proof.t
+
+(** Proof entries represent a proof that has been finished, but still
+   not registered with the kernel.
+
+   XXX: Scheduled for removal from public API, don't rely on it *)
+type 'a proof_entry = private {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Id.Set.t 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;
+}
+
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type proof_object = private
+  { 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 -> Proof.t -> proof_object
+
+(** Declaration of local constructions (Variable/Hypothesis/Local) *)
+
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type variable_declaration =
+  | SectionLocalDef of Evd.side_effects proof_entry
+  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
+
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type 'a constant_entry =
+  | DefinitionEntry of 'a proof_entry
+  | ParameterEntry of parameter_entry
+  | PrimitiveEntry of primitive_entry
+
+val declare_variable
+  :  name:variable
+  -> kind:Decls.logical_kind
+  -> variable_declaration
+  -> unit
+
+(** Declaration of global constructions
+   i.e. Definition/Theorem/Axiom/Parameter/...
+
+   XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+val definition_entry
+  : ?fix_exn:Future.fix_exn
+  -> ?opaque:bool
+  -> ?inline:bool
+  -> ?feedback_id:Stateid.t
+  -> ?section_vars:Id.Set.t
+  -> ?types:types
+  -> ?univs:Entries.universes_entry
+  -> ?eff:Evd.side_effects
+  -> ?univsbody:Univ.ContextSet.t
+  (** Universe-constraints attached to the body-only, used in
+     vio-delayed opaque constants and private poly universes *)
+  -> constr
+  -> Evd.side_effects proof_entry
+
+(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+val pure_definition_entry
+  : ?fix_exn:Future.fix_exn
+  -> ?opaque:bool
+  -> ?inline:bool
+  -> ?types:types
+  -> ?univs:Entries.universes_entry
+  -> constr
+  -> unit proof_entry
+
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
+(** [declare_constant id cd] declares a global declaration
+   (constant/parameter) with name [id] in the current section; it returns
+   the full path of the declaration
+
+  internal specify if the constant has been created by the kernel or by the
+  user, and in the former case, if its errors should be silent
+
+  XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+val declare_constant
+  :  ?local:import_status
+  -> name:Id.t
+  -> kind:Decls.logical_kind
+  -> Evd.side_effects constant_entry
+  -> Constant.t
+
+val declare_private_constant
+  :  ?role:Evd.side_effect_role
+  -> ?local:import_status
+  -> name:Id.t
+  -> kind:Decls.logical_kind
+  -> unit proof_entry
+  -> Constant.t * Evd.side_effects
+
+(** [inline_private_constants ~sideff ~uctx env ce] will inline the
+   constants in [ce]'s body and return the body plus the updated
+   [UState.t].
+
+   XXX: Scheduled for removal from public API, don't rely on it *)
+val inline_private_constants
+  :  uctx:UState.t
+  -> Environ.env
+  -> Evd.side_effects proof_entry
+  -> Constr.t * UState.t
+
+(** Declaration messages *)
+
+(** XXX: Scheduled for removal from public API, do not use *)
+val definition_message : Id.t -> unit
+val assumption_message : Id.t -> unit
+val fixpoint_message : int array option -> Id.t list -> unit
+val recursive_message : bool (** true = fixpoint *) ->
+  int array option -> Id.t list -> unit
+
+val check_exists : Id.t -> unit
+
+(* Used outside this module only in indschemes *)
+exception AlreadyDeclared of (string option * Id.t)
+
+(** {6 For legacy support, do not use}  *)
+
+module Internal : sig
+
+  val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
+  val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
+  (* Overriding opacity is indeed really hacky *)
+  val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
+
+  (* TODO: This is only used in DeclareDef to forward the fix to
+     hooks, should eventually go away *)
+  val get_fix_exn : 'a proof_entry -> Future.fix_exn
+
+  val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
+
+  type constant_obj
+
+  val objConstant : constant_obj Libobject.Dyn.tag
+  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 : 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 : Proof.t -> closed_proof_output
+val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
+
+(** [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.t -> Proof.t * bool
+
+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 Helpers to obtain proof state when in an interactive proof } *)
+
+(** [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.t -> int -> Evd.evar_map * Environ.env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+val get_current_goal_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 : Proof.t -> Evd.evar_map * Environ.env
+
+(** Temporarily re-exported for 3rd party code; don't use  *)
+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
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 20fa43c8e7..89f3503f4d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -94,7 +94,7 @@ let do_universe ~poly l =
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
   let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
-  Declare.declare_universe_context ~poly ctx
+  DeclareUctx.declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
   let open Univ in
@@ -107,4 +107,4 @@ let do_constraint ~poly l =
       Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  Declare.declare_universe_context ~poly uctx
+  DeclareUctx.declare_universe_context ~poly uctx
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 3d3be8050d..6d5d16d94a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -9,6 +9,7 @@ Himsg
 Locality
 Egramml
 Vernacextend
+Declare
 ComHints
 Ppvernac
 Proof_using
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 028a7d0859..4958d0116e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1719,7 +1719,8 @@ let vernac_print ~pstate ~atts =
   | PrintHintGoal ->
      begin match pstate with
      | Some pstate ->
-       Hints.pr_applicable_hint pstate
+       let pf = Declare.Proof.get_proof pstate in
+       Hints.pr_applicable_hint pf
      | None ->
        str "No proof in progress"
      end
-- 
cgit v1.2.3