Move Declare to tactics folder.

Nobody really knows where this module should belong, it seems. My personal
theory is that it should live in vernac instead, but due to nasty
interactions with abstract-like tactics, we have to put it somewhere below.

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