Merge PR #10406: Desynchronize the type of proof and kernel entries

Reviewed-by: ejgallego
Reviewed-by: gares

7 files changed, 769 insertions, 21 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 8f66032873..e4fa5e84b4 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -70,19 +70,19 @@ let rec shrink ctx sign c t accu =
 | _ -> assert false
 
 let shrink_entry sign const =
-  let open Entries in
-  let typ = match const.const_entry_type with
+  let open Proof_global in
+  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.const_entry_body) in
-  let ((body, uctx), eff) = Future.force const.const_entry_body in
+  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
   let const = { const with
-    const_entry_body = Future.from_val ((body, uctx), eff);
-    const_entry_type = Some typ;
+    proof_entry_body = Future.from_val ((body, uctx), eff);
+    proof_entry_type = Some typ;
   } in
   (const, args)
 
@@ -152,7 +152,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+  let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
   let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
@@ -161,20 +161,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
-  let inst = match const.Entries.const_entry_universes with
+  let inst = match const.Proof_global.proof_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
     (* We mimic what the kernel does, that is ensuring that no additional
        constraints appear in the body of polymorphic constants. Ideally this
        should be enforced statically. *)
-    let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
+    let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in
     let () = assert (Univ.ContextSet.is_empty body_uctx) in
     EInstance.make (Univ.UContext.instance ctx)
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let effs = Evd.concat_side_effects eff
-    Entries.(snd (Future.force const.const_entry_body)) in
+    Proof_global.(snd (Future.force const.proof_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index c474a01d1c..e278729f89 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P
    save path *)
 val shrink_entry
   :  ('a, 'b) Context.Named.Declaration.pt list
-  -> 'c Entries.definition_entry
-  -> 'c Entries.definition_entry * Constr.t list
+  -> 'c Proof_global.proof_entry
+  -> 'c Proof_global.proof_entry * Constr.t list
diff --git a/tactics/declare.ml b/tactics/declare.ml
new file mode 100644
index 0000000000..fdb8155038
--- /dev/null
+++ b/tactics/declare.ml
@@ -0,0 +1,651 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** This module is about the low-level declaration of logical objects *)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Libnames
+open Globnames
+open Constr
+open Declarations
+open Entries
+open Libobject
+open Lib
+open Impargs
+open Safe_typing
+open Cooking
+open Decls
+open Decl_kinds
+
+(** flag for internal message display *)
+type internal_flag =
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
+
+(** Declaration of constants and parameters *)
+
+type constant_obj = {
+  cst_decl : Cooking.recipe option;
+  (** Non-empty only when rebuilding a constant after a section *)
+  cst_kind : logical_kind;
+  cst_locl : import_status;
+}
+
+type 'a constant_entry =
+  | DefinitionEntry of 'a Proof_global.proof_entry
+  | ParameterEntry of parameter_entry
+  | PrimitiveEntry of primitive_entry
+
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
+
+(* 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
+    alreadydeclared (Id.print (basename sp) ++ str " already exists");
+  let con = Global.constant_of_delta_kn kn in
+  Nametab.push (Nametab.Until i) sp (ConstRef con);
+  add_constant_kind con obj.cst_kind
+
+let cooking_info segment =
+  let modlist = replacement_context () in
+  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in
+  let named_ctx = List.map fst hyps in
+  let abstract = (named_ctx, subst, uctx) in
+  { Opaqueproof.modlist; abstract }
+
+(* Opening means making the name without its module qualification available *)
+let open_constant 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
+    Nametab.push (Nametab.Exactly i) sp (ConstRef con)
+
+let exists_name id =
+  variable_exists id || Global.exists_objlabel (Label.of_id id)
+
+let check_exists id =
+  if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
+
+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 id = basename sp in
+  let kn' =
+    match obj.cst_decl with
+    | None ->
+      if Global.exists_objlabel (Label.of_id (basename sp))
+      then Constant.make1 kn
+      else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".")
+    | Some r ->
+      Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r
+  in
+  assert (Constant.equal kn' (Constant.make1 kn));
+  Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
+  let cst = Global.lookup_constant kn' in
+  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
+  add_constant_kind (Constant.make1 kn) obj.cst_kind
+
+let discharge_constant ((sp, kn), obj) =
+  let con = Constant.make1 kn in
+  let from = Global.lookup_constant con in
+  let info = cooking_info (section_segment_of_constant con) in
+  (* This is a hack: when leaving a section, we lose the constant definition, so
+     we have to store it in the libobject to be able to retrieve it after. *)
+  Some { obj with cst_decl = Some { from; info } }
+
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_constant cst = {
+  cst_decl = None;
+  cst_kind = cst.cst_kind;
+  cst_locl = cst.cst_locl;
+}
+
+let classify_constant cst = Substitute (dummy_constant cst)
+
+let (inConstant : constant_obj -> obj) =
+  declare_object { (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 declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+
+let update_tables c =
+  declare_constant_implicits c;
+  Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
+
+let register_constant kn kind local =
+  let o = inConstant {
+    cst_decl = None;
+    cst_kind = kind;
+    cst_locl = local;
+  } in
+  let id = Label.to_id (Constant.label kn) in
+  let _ = add_leaf id o in
+  update_tables kn
+
+let register_side_effect (c, role) =
+  let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in
+  match role with
+  | None -> ()
+  | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
+
+let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
+  let open Proof_global in
+  { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
+    proof_entry_secctx = None;
+    proof_entry_type = types;
+    proof_entry_universes = univs;
+    proof_entry_opaque = opaque;
+    proof_entry_feedback = None;
+    proof_entry_inline_code = inline}
+
+let cast_proof_entry e =
+  let open Proof_global in
+  let (body, ctx), () = Future.force e.proof_entry_body in
+  {
+    const_entry_body = (body, ctx);
+    const_entry_secctx = e.proof_entry_secctx;
+    const_entry_feedback = e.proof_entry_feedback;
+    const_entry_type = e.proof_entry_type;
+    const_entry_universes = e.proof_entry_universes;
+    const_entry_inline_code = e.proof_entry_inline_code;
+  }
+
+let cast_opaque_proof_entry e =
+  let open Proof_global in
+  let typ = match e.proof_entry_type with
+  | None -> assert false
+  | Some typ -> typ
+  in
+  {
+    opaque_entry_body = e.proof_entry_body;
+    opaque_entry_secctx = e.proof_entry_secctx;
+    opaque_entry_feedback = e.proof_entry_feedback;
+    opaque_entry_type = typ;
+    opaque_entry_universes = e.proof_entry_universes;
+  }
+
+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 define_constant ~side_effect ?(export_seff=false) id cd =
+  let open Proof_global in
+  (* Logically define the constant and its subproofs, no libobject tampering *)
+  let is_poly de = match de.proof_entry_universes with
+  | Monomorphic_entry _ -> false
+  | Polymorphic_entry _ -> true
+  in
+  let in_section = Lib.sections_are_opened () in
+  let export, decl = (* We deal with side effects *)
+    match cd with
+    | DefinitionEntry de when
+        export_seff ||
+        not de.proof_entry_opaque ||
+        is_poly de ->
+      (* This globally defines the side-effects in the environment. *)
+      let body, eff = Future.force de.proof_entry_body in
+      let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+      let export = get_roles export eff in
+      let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+      let cd = match de.proof_entry_opaque with
+      | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de)
+      | false -> Entries.DefinitionEntry (cast_proof_entry de)
+      in
+      export, ConstantEntry (PureEntry, cd)
+    | DefinitionEntry de ->
+      let () = assert (de.proof_entry_opaque) in
+      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 de in
+      [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
+    | ParameterEntry e ->
+      [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
+    | PrimitiveEntry e ->
+      [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
+  in
+  let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
+  kn, eff, export
+
+let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) =
+  let () = check_exists id in
+  let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in
+  (* Register the libobjects attached to the constants and its subproofs *)
+  let () = List.iter register_side_effect export in
+  let () = register_constant kn kind local in
+  kn
+
+let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
+  let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
+  let () = assert (List.is_empty export) 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 declare_definition ?(internal=UserIndividualRequest)
+  ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior)
+  id ?types (body,univs) =
+  let cb =
+    definition_entry ?types ~univs ~opaque body
+  in
+    declare_constant ~internal ~local id
+      (DefinitionEntry cb, Decl_kinds.IsDefinition kind)
+
+(** Declaration of section variables and local definitions *)
+type section_variable_entry =
+  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+
+type variable_declaration = DirPath.t * section_variable_entry * logical_kind
+
+let cache_variable ((sp,_),o) =
+  match o with
+  | Inl ctx -> Global.push_context_set false ctx
+  | Inr (id,(p,d,mk)) ->
+  (* Constr raisonne sur les noms courts *)
+  if variable_exists id then
+    alreadydeclared (Id.print id ++ str " already exists");
+
+  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum ((ty,ctx),poly,impl) ->
+      let () = Global.push_named_assum ((id,ty,poly),ctx) in
+      let impl = if impl then Implicit else Explicit in
+        impl, true, poly, ctx
+    | SectionLocalDef (de) ->
+      (* The body should already have been forced upstream because it is a
+         section-local definition, but it's not enforced by typing *)
+      let open Proof_global in
+      let (body, eff) = Future.force de.proof_entry_body in
+      let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+      let eff = get_roles export eff in
+      let () = List.iter register_side_effect eff in
+      let poly, univs = match de.proof_entry_universes with
+      | Monomorphic_entry uctx -> false, uctx
+      | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+      in
+      let univs = Univ.ContextSet.union uctx univs in
+      (* We must declare the universe constraints before type-checking the
+         term. *)
+      let () = Global.push_context_set (not poly) univs in
+      let se = {
+        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 (id, se) in
+      Explicit, de.proof_entry_opaque,
+      poly, univs in
+  Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
+  add_section_variable id impl poly ctx;
+  add_variable_data id (p,opaq,ctx,poly,mk)
+
+let discharge_variable (_,o) = match o with
+  | Inr (id,_) ->
+    if variable_polymorphic id then None
+    else Some (Inl (variable_context id))
+  | Inl _ -> Some o
+
+type variable_obj =
+    (Univ.ContextSet.t, Id.t * variable_declaration) union
+
+let inVariable : variable_obj -> obj =
+  declare_object { (default_object "VARIABLE") with
+    cache_function = cache_variable;
+    discharge_function = discharge_variable;
+    classify_function = (fun _ -> Dispose) }
+
+(* for initial declaration *)
+let declare_variable id obj =
+  let oname = add_leaf id (inVariable (Inr (id,obj))) in
+  declare_var_implicits id;
+  Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
+  oname
+
+(** Declaration of inductive blocks *)
+let declare_inductive_argument_scopes kn mie =
+  List.iteri (fun i {mind_entry_consnames=lc} ->
+    Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i));
+    for j=1 to List.length lc do
+      Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j));
+    done) mie.mind_entry_inds
+
+let inductive_names sp kn mie =
+  let (dp,_) = repr_path sp in
+  let kn = Global.mind_of_delta_kn kn in
+  let names, _ =
+    List.fold_left
+      (fun (names, n) ind ->
+         let ind_p = (kn,n) in
+         let names, _ =
+           List.fold_left
+             (fun (names, p) l ->
+                let sp =
+                  Libnames.make_path dp l
+                in
+                  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
+             (names, 1) ind.mind_entry_consnames in
+         let sp = Libnames.make_path dp ind.mind_entry_typename
+         in
+           ((sp, IndRef ind_p) :: names, n+1))
+      ([], 0) mie.mind_entry_inds
+  in names
+
+let load_inductive i ((sp,kn),mie) =
+  let names = inductive_names sp kn mie in
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
+
+let open_inductive i ((sp,kn),mie) =
+  let names = inductive_names sp kn mie in
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
+
+let cache_inductive ((sp,kn),mie) =
+  let names = inductive_names sp kn mie in
+  List.iter check_exists (List.map (fun p -> basename (fst p)) names);
+  let id = basename sp in
+  let kn' = Global.add_mind id mie in
+  assert (MutInd.equal kn' (MutInd.make1 kn));
+  let mind = Global.lookup_mind kn' in
+  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp,kn),mie) =
+  let mind = Global.mind_of_delta_kn kn in
+  let mie = Global.lookup_mind mind in
+  let info = cooking_info (section_segment_of_mutual_inductive mind) in
+  Some (Cooking.cook_inductive info mie)
+
+let dummy_one_inductive_entry mie = {
+  mind_entry_typename = mie.mind_entry_typename;
+  mind_entry_arity = mkProp;
+  mind_entry_template = false;
+  mind_entry_consnames = mie.mind_entry_consnames;
+  mind_entry_lc = []
+}
+
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_inductive_entry m = {
+  mind_entry_params = [];
+  mind_entry_record = None;
+  mind_entry_finite = Declarations.BiFinite;
+  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
+  mind_entry_universes = default_univ_entry;
+  mind_entry_variance = None;
+  mind_entry_private = None;
+}
+
+(* reinfer subtyping constraints for inductive after section is dischared. *)
+let rebuild_inductive mind_ent =
+  let env = Global.env () in
+  InferCumulativity.infer_inductive env mind_ent
+
+let inInductive : mutual_inductive_entry -> obj =
+  declare_object {(default_object "INDUCTIVE") with
+    cache_function = cache_inductive;
+    load_function = load_inductive;
+    open_function = open_inductive;
+    classify_function = (fun a -> Substitute (dummy_inductive_entry a));
+    subst_function = ident_subst_function;
+    discharge_function = discharge_inductive;
+    rebuild_function = rebuild_inductive }
+
+let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+
+let load_prim _ p = cache_prim p
+
+let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c
+
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
+
+let inPrim : (Projection.Repr.t * Constant.t) -> obj =
+  declare_object {
+    (default_object "PRIMPROJS") with
+    cache_function = cache_prim ;
+    load_function = load_prim;
+    subst_function = subst_prim;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_prim }
+
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
+
+let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
+  let id = Label.to_id label in
+  let univs, u = match univs with
+    | Monomorphic_entry _ ->
+      (* Global constraints already defined through the inductive *)
+      default_univ_entry, Univ.Instance.empty
+    | Polymorphic_entry (nas, ctx) ->
+      Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
+  in
+  let term = Vars.subst_instance_constr u term in
+  let types = Vars.subst_instance_constr u types in
+  let entry = definition_entry ~types ~univs term in
+  let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+  declare_primitive_projection p cst
+
+
+let declare_projections univs mind =
+  let env = Global.env () in
+  let mib = Environ.lookup_mind mind env in
+  match mib.mind_record with
+  | PrimRecord info ->
+    let iter_ind i (_, labs, _, _) =
+      let ind = (mind, i) in
+      let projs = Inductiveops.compute_projections env ind in
+      Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
+    in
+    let () = Array.iteri iter_ind info in
+    true
+  | FakeRecord -> false
+  | NotRecord -> false
+
+(* for initial declaration *)
+let declare_mind mie =
+  let id = match mie.mind_entry_inds with
+    | ind::_ -> ind.mind_entry_typename
+    | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
+  let (sp,kn as oname) = add_leaf id (inInductive mie) in
+  let mind = Global.mind_of_delta_kn kn in
+  let isprim = declare_projections mie.mind_entry_universes mind in
+  declare_mib_implicits mind;
+  declare_inductive_argument_scopes mind mie;
+  oname, isprim
+
+(* Declaration messages *)
+
+let pr_rank i = pr_nth (i+1)
+
+let fixpoint_message indexes l =
+  Flags.if_verbose Feedback.msg_info (match l with
+  | [] -> 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
+  | [] -> 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")
+
+(** Monomorphic universes need to survive sections. *)
+
+let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
+  declare_object @@ local_object "Monomorphic section universes"
+    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
+    ~discharge:(fun (_, x) -> Some x)
+
+let declare_universe_context poly ctx =
+  if poly then
+    (Global.push_context_set true ctx; Lib.add_section_context ctx)
+  else
+    Lib.add_anonymous_leaf (input_universe_context ctx)
+
+(** Global universes are not substitutive objects but global objects
+   bound at the *library* or *module* level. The polymorphic flag is
+   used to distinguish universes declared in polymorphic sections, which
+   are discharged and do not remain in scope. *)
+
+type universe_source =
+  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
+  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
+  | UnqualifiedUniv (* other global universe *)
+
+type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
+
+let check_exists sp =
+  if Nametab.exists_universe sp then
+    alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
+  else ()
+
+let qualify_univ i dp src id =
+  match src with
+  | BoundUniv | UnqualifiedUniv ->
+    i,  Libnames.make_path dp id
+  | QualifiedUniv l ->
+    let dp = DirPath.repr dp in
+    Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
+
+let do_univ_name ~check i dp src (id,univ) =
+  let i, sp = qualify_univ i dp src id in
+  if check then check_exists sp;
+  Nametab.push_universe i sp univ
+
+let cache_univ_names ((sp, _), (src, univs)) =
+  let depth = sections_depth () in
+  let dp = pop_dirpath_n depth (dirpath sp) in
+  List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
+
+let load_univ_names i ((sp, _), (src, univs)) =
+  List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs
+
+let open_univ_names i ((sp, _), (src, univs)) =
+  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs
+
+let discharge_univ_names = function
+  | _, (BoundUniv, _) -> None
+  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
+
+let input_univ_names : universe_name_decl -> Libobject.obj =
+  declare_object
+    { (default_object "Global universe name state") with
+      cache_function = cache_univ_names;
+      load_function = load_univ_names;
+      open_function = open_univ_names;
+      discharge_function = discharge_univ_names;
+      subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
+      classify_function = (fun a -> Substitute a) }
+
+let declare_univ_binders gr pl =
+  if Global.is_polymorphic gr then
+    ()
+  else
+    let l = match gr with
+      | ConstRef c -> Label.to_id @@ Constant.label c
+      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+      | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
+      | ConstructRef _ ->
+        anomaly ~label:"declare_univ_binders"
+          Pp.(str "declare_univ_binders on an constructor reference")
+    in
+    let univs = Id.Map.fold (fun id univ univs ->
+        match Univ.Level.name univ with
+        | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+        | Some univ -> (id,univ)::univs) pl []
+    in
+    Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
+
+let do_universe poly l =
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err ~hdr:"Constraint"
+                   (str"Cannot declare polymorphic universes outside sections")
+  in
+  let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
+  let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
+      Univ.LSet.empty l, Univ.Constraint.empty
+  in
+  let () = declare_universe_context poly ctx in
+  let src = if poly then BoundUniv else UnqualifiedUniv in
+  Lib.add_anonymous_leaf (input_univ_names (src, l))
+
+let do_constraint poly l =
+  let open Univ in
+  let u_of_id x =
+    let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
+    Lib.is_polymorphic_univ level, level
+  in
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err ~hdr:"Constraint"
+                    (str"Cannot declare polymorphic constraints outside sections")
+  in
+  let check_poly p p' =
+    if poly then ()
+    else if p || p' then
+      user_err ~hdr:"Constraint"
+                    (str "Cannot declare a global constraint on " ++
+                    str "a polymorphic universe, use "
+                    ++ str "Polymorphic Constraint instead")
+  in
+  let constraints = List.fold_left (fun acc (l, d, r) ->
+     let p, lu = u_of_id l and p', ru = u_of_id r in
+     check_poly p p';
+     Constraint.add (lu, d, ru) acc)
+    Constraint.empty l
+  in
+  let uctx = ContextSet.add_constraints constraints ContextSet.empty in
+  declare_universe_context poly uctx
diff --git a/tactics/declare.mli b/tactics/declare.mli
new file mode 100644
index 0000000000..692eca8dde
--- /dev/null
+++ b/tactics/declare.mli
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Constr
+open Entries
+open Decl_kinds
+
+(** This module provides the official functions to declare new variables,
+   parameters, constants and inductive types. Using the following functions
+   will add the entries in the global environment (module [Global]), will
+   register the declarations in the library (module [Lib]) --- so that the
+   reset works properly --- and will fill some global tables such as
+   [Nametab] and [Impargs]. *)
+
+(** Declaration of local constructions (Variable/Hypothesis/Local) *)
+
+type section_variable_entry =
+  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+
+type 'a constant_entry =
+  | DefinitionEntry of 'a Proof_global.proof_entry
+  | ParameterEntry of parameter_entry
+  | PrimitiveEntry of primitive_entry
+
+type variable_declaration = DirPath.t * section_variable_entry * logical_kind
+
+val declare_variable : variable -> variable_declaration -> Libobject.object_name
+
+(** Declaration of global constructions
+   i.e. Definition/Theorem/Axiom/Parameter/... *)
+
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
+
+type internal_flag =
+  | UserAutomaticRequest
+  | InternalTacticRequest
+  | UserIndividualRequest
+
+(* Default definition entries, transparent with no secctx or proj information *)
+val definition_entry : ?fix_exn:Future.fix_exn ->
+  ?opaque:bool -> ?inline:bool -> ?types:types ->
+  ?univs:Entries.universes_entry ->
+  ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
+
+(** [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 *)
+val declare_constant :
+ ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
+
+val declare_private_constant :
+  ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
+
+val declare_definition :
+  ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
+  ?local:import_status -> Id.t -> ?types:constr ->
+  constr Entries.in_universes_entry -> Constant.t
+
+(** Since transparent constants' side effects are globally declared, we
+ *  need that *)
+val set_declare_scheme :
+  (string -> (inductive * Constant.t) array -> unit) -> unit
+
+(** [declare_mind me] declares a block of inductive types with
+   their constructors in the current section; it returns the path of
+   the whole block and a boolean indicating if it is a primitive record. *)
+val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
+
+(** Declaration messages *)
+
+val definition_message : Id.t -> unit
+val assumption_message : Id.t -> unit
+val fixpoint_message : int array option -> Id.t list -> unit
+val cofixpoint_message : Id.t list -> unit
+val recursive_message : bool (** true = fixpoint *) ->
+  int array option -> Id.t list -> unit
+
+val exists_name : Id.t -> bool
+
+(** Global universe contexts, names and constraints *)
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
+
+val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
+
+val do_universe : polymorphic -> lident list -> unit
+val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9b8ad8191e..8526bdd373 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -23,7 +23,6 @@ open Constr
 open CErrors
 open Util
 open Declare
-open Entries
 open Decl_kinds
 open Pp
 
@@ -122,15 +121,15 @@ let define internal role id c poly univs =
   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 = {
-    const_entry_body =
+    Proof_global.proof_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
                        Evd.empty_side_effects);
-    const_entry_secctx = None;
-    const_entry_type = None;
-    const_entry_universes = univs;
-    const_entry_opaque = false;
-    const_entry_inline_code = false;
-    const_entry_feedback = None;
+    proof_entry_secctx = None;
+    proof_entry_type = None;
+    proof_entry_universes = univs;
+    proof_entry_opaque = false;
+    proof_entry_inline_code = false;
+    proof_entry_feedback = None;
   } in
   let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 61608c577c..d8f4b66d0e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -22,7 +22,6 @@ open Namegen
 open Evd
 open Printer
 open Reductionops
-open Entries
 open Inductiveops
 open Tacmach.New
 open Clenv
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 1861c5b99b..6dd749aa0d 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,3 +1,4 @@
+Declare
 Dnet
 Dn
 Btermdn