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

Reviewed-by: ejgallego
Reviewed-by: gares

3 files changed, 0 insertions, 703 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
deleted file mode 100644
index 77313a54de..0000000000
--- a/interp/declare.ml
+++ /dev/null
@@ -1,609 +0,0 @@
-(************************************************************************)
-(*         *   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 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 =
-  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
-    const_entry_secctx = None;
-    const_entry_type = types;
-    const_entry_universes = univs;
-    const_entry_opaque = opaque;
-    const_entry_feedback = None;
-    const_entry_inline_code = inline}
-
-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 =
-  (* Logically define the constant and its subproofs, no libobject tampering *)
-  let is_poly de = match de.const_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.const_entry_opaque ||
-        is_poly de ->
-      (* This globally defines the side-effects in the environment. *)
-      let body, eff = Future.force de.const_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 const_entry_body = Future.from_val (body, ()) } in
-      export, ConstantEntry (PureEntry, DefinitionEntry de)
-    | DefinitionEntry de ->
-      let map (body, eff) = body, eff.Evd.seff_private in
-      let body = Future.chain de.const_entry_body map in
-      let de = { de with const_entry_body = body } in
-      [], ConstantEntry (EffectEntry, DefinitionEntry de)
-    | ParameterEntry _ | PrimitiveEntry _ as cd ->
-      [], ConstantEntry (PureEntry, cd)
-  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
-      (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
-
-(** Declaration of section variables and local definitions *)
-type section_variable_entry =
-  | SectionLocalDef of Evd.side_effects definition_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 (body, eff) = Future.force de.const_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.const_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.const_entry_secctx;
-        secdef_feedback = de.const_entry_feedback;
-        secdef_type = de.const_entry_type;
-      } in
-      let () = Global.push_named_def (id, se) in
-      Explicit, de.const_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/interp/declare.mli b/interp/declare.mli
deleted file mode 100644
index 0f64235048..0000000000
--- a/interp/declare.mli
+++ /dev/null
@@ -1,93 +0,0 @@
-(************************************************************************)
-(*         *   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 definition_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
-
-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 definition_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/interp/interp.mllib b/interp/interp.mllib
index 52978a2ab6..33573edcce 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -17,4 +17,3 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Declare