Merge PR #10950: [declare] Split universe and inductive declaration code to vernac/

Ack-by: Janno
Reviewed-by: SkySkimmer

15 files changed, 390 insertions, 335 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 7d32f1a7e8..57eeddb847 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -266,6 +266,7 @@ let get_roles export eff =
   List.map map export
 
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
+
 let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
@@ -375,132 +376,6 @@ let declare_variable ~name ~kind d =
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
-(** 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 (GlobRef.IndRef (kn,i));
-    for j=1 to List.length lc do
-      Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j));
-    done) mie.mind_entry_inds
-
-type inductive_obj = {
-  ind_names : (Id.t * Id.t list) list
-  (* For each block, name of the type + name of constructors *)
-}
-
-let inductive_names sp kn obj =
-  let (dp,_) = Libnames.repr_path sp in
-  let kn = Global.mind_of_delta_kn kn in
-  let names, _ =
-    List.fold_left
-      (fun (names, n) (typename, consnames) ->
-         let ind_p = (kn,n) in
-         let names, _ =
-           List.fold_left
-             (fun (names, p) l ->
-                let sp =
-                  Libnames.make_path dp l
-                in
-                  ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
-             (names, 1) consnames in
-         let sp = Libnames.make_path dp typename
-         in
-           ((sp, GlobRef.IndRef ind_p) :: names, n+1))
-      ([], 0) obj.ind_names
-  in names
-
-let load_inductive i ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
-
-let open_inductive i ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
-
-let cache_inductive ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
-
-let discharge_inductive ((sp, kn), names) =
-  Some names
-
-let inInductive : inductive_obj -> obj =
-  declare_object {(default_object "INDUCTIVE") with
-    cache_function = cache_inductive;
-    load_function = load_inductive;
-    open_function = open_inductive;
-    classify_function = (fun a -> Substitute a);
-    subst_function = ident_subst_function;
-    discharge_function = discharge_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 name = 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 ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) 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
-    | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
-  let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
-  let names = List.map map_names mie.mind_entry_inds in
-  List.iter (fun (typ, cons) -> check_exists typ; List.iter check_exists cons) names;
-  let _kn' = Global.add_mind id mie in
-  let (sp,kn as oname) = add_leaf id (inInductive { ind_names = names }) in
-  if is_unsafe_typing_flags() then feedback_axiom();
-  let mind = Global.mind_of_delta_kn kn in
-  let isprim = declare_projections mie.mind_entry_universes mind in
-  Impargs.declare_mib_implicits mind;
-  declare_inductive_argument_scopes mind mie;
-  oname, isprim
-
 (* Declaration messages *)
 
 let pr_rank i = pr_nth (i+1)
@@ -538,106 +413,3 @@ let assumption_message id =
   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")
-
-(** 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_universe sp =
-  if Nametab.exists_universe sp then
-    raise (AlreadyDeclared (Some "Universe", Libnames.basename sp))
-  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_universe sp;
-  Nametab.push_universe i sp univ
-
-let cache_univ_names ((sp, _), (src, univs)) =
-  let depth = sections_depth () in
-  let dp = Libnames.pop_dirpath_n depth (Libnames.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) (Libnames.dirpath sp) src) univs
-
-let open_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.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 = let open GlobRef in match gr with
-      | ConstRef c -> Label.to_id @@ Constant.label c
-      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
-      | VarRef id ->
-        CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
-      | ConstructRef _ ->
-        CErrors.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 = Global.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      CErrors.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 src = if poly then BoundUniv else UnqualifiedUniv in
-  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
-  declare_universe_context ~poly ctx
-
-let do_constraint ~poly l =
-  let open Univ in
-  let u_of_id x =
-    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
-  in
-  let constraints = List.fold_left (fun acc (l, d, r) ->
-      let lu = u_of_id l and ru = u_of_id r in
-      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
index a6c1374a77..1a037ef937 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -43,6 +43,8 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
+
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
@@ -86,11 +88,6 @@ val declare_private_constant
 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
@@ -100,15 +97,7 @@ 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 : poly:bool -> Univ.ContextSet.t -> unit
-
-val do_universe : poly:bool -> lident list -> unit
-val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
+val check_exists : Id.t -> unit
 
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 702a3e44a9..09866a75c9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -325,7 +325,7 @@ let declare_instance_constant info global imps ?hook name decl poly sigma term t
   let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
   let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
   Declare.definition_message name;
-  Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
+  DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
   instance_hook info global imps ?hook (GlobRef.ConstRef kn)
 
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
@@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam
   let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
-  Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
+  DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
   instance_hook pri global imps (GlobRef.ConstRef cst)
 
 let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a0b0dcf4c8..e5db6146ca 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -69,7 +69,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
   let kn = Declare.declare_constant ~name ~local ~kind decl in
   let gr = GlobRef.ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Declare.declare_univ_binders gr pl in
+  let () = DeclareUniv.declare_univ_binders gr pl in
   let () = Declare.assumption_message name in
   let env = Global.env () in
   let sigma = Evd.from_env env in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 98b869d72e..cee5b7c1f4 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -15,18 +15,15 @@ open Util
 open Constr
 open Context
 open Environ
-open Declare
 open Names
 open Libnames
 open Nameops
 open Constrexpr
 open Constrexpr_ops
 open Constrintern
-open Impargs
 open Reductionops
 open Type_errors
 open Pretyping
-open Indschemes
 open Context.Rel.Declaration
 open Entries
 
@@ -80,12 +77,6 @@ type structured_one_inductive_expr = {
   ind_lc : (Id.t * constr_expr) list
 }
 
-let minductive_message = function
-  | []  -> user_err Pp.(str "No inductive definition.")
-  | [x] -> (Id.print x ++ str " is defined")
-  | l   -> hov 0  (prlist_with_sep pr_comma Id.print l ++
-                     spc () ++ str "are defined")
-
 let check_all_names_different indl =
   let ind_names = List.map (fun ind -> ind.ind_name) indl in
   let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
@@ -541,62 +532,6 @@ let extract_mutual_inductive_declaration_components indl =
   let indl = extract_inductive indl in
   (params,indl), coes, List.flatten ntnl
 
-let is_recursive mie =
-  let rec is_recursive_constructor lift typ =
-    match Constr.kind typ with
-    | Prod (_,arg,rest) ->
-        not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) ||
-        is_recursive_constructor (lift+1) rest
-    | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
-    | _ -> false
-  in
-  match mie.mind_entry_inds with
-  | [ind] ->
-      let nparams = List.length mie.mind_entry_params in
-      List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc
-  | _ -> false
-
-let warn_non_primitive_record =
-  CWarnings.create ~name:"non-primitive-record" ~category:"record"
-         (fun indsp ->
-          (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++
-                    strbrk" could not be defined as a primitive record")))
-
-let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
-  (* spiwack: raises an error if the structure is supposed to be non-recursive,
-        but isn't *)
-  begin match mie.mind_entry_finite with
-  | Declarations.BiFinite when is_recursive mie ->
-      if Option.has_some mie.mind_entry_record then
-        user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
-      else
-        user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command."))
-  | _ -> ()
-  end;
-  let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let (_, kn), prim = declare_mind mie in
-  let mind = Global.mind_of_delta_kn kn in
-  if primitive_expected && not prim then warn_non_primitive_record (mind,0);
-  Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
-  List.iteri (fun i (indimpls, constrimpls) ->
-              let ind = (mind,i) in
-              let gr = GlobRef.IndRef ind in
-              maybe_declare_manual_implicits false gr indimpls;
-              List.iteri
-                (fun j impls ->
-                 maybe_declare_manual_implicits false
-                    (GlobRef.ConstructRef (ind, succ j)) impls)
-                constrimpls)
-      impls;
-  Flags.if_verbose Feedback.msg_info (minductive_message names);
-  if mie.mind_entry_private == None
-  then declare_default_schemes mind;
-  mind
-
-type one_inductive_impls =
-  Impargs.manual_implicits (* for inds *) *
-  Impargs.manual_implicits list (* for constrs *)
-
 type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
@@ -607,7 +542,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
   let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
   let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (declare_mutual_inductive_with_eliminations mie pl impls);
+  ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
@@ -652,3 +587,5 @@ let make_cases ind =
        let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
        (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
     mip.mind_nf_lc []
+
+let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 7587bd165f..067fb3d2ca 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Entries
 open Vernacexpr
 open Constrexpr
 
@@ -42,22 +41,18 @@ val do_mutual_inductive
 
 val make_cases : Names.inductive -> string list list
 
+val declare_mutual_inductive_with_eliminations
+  : ?primitive_expected:bool
+  -> Entries.mutual_inductive_entry
+  -> UnivNames.universe_binders
+  -> DeclareInd.one_inductive_impls list
+  -> Names.MutInd.t
+  [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
+
 (************************************************************************)
 (** Internal API, exported for Record                                   *)
 (************************************************************************)
 
-(** Registering a mutual inductive definition together with its
-   associated schemes *)
-
-type one_inductive_impls =
-  Impargs.manual_implicits (* for inds *) *
-  Impargs.manual_implicits list (* for constrs *)
-
-val declare_mutual_inductive_with_eliminations :
-  ?primitive_expected:bool ->
-  mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
-  MutInd.t
-
 val should_auto_template : Id.t -> bool -> bool
 (** [should_auto_template x b] is [true] when [b] is [true] and we
    automatically use template polymorphism. [x] is the name of the
@@ -72,7 +67,3 @@ val template_polymorphism_candidate :
    can be made parametric in its conclusion sort, if one is given.
    If the [Template Check] flag is false we just check that the conclusion sort
    is not small. *)
-
-val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
-(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
-    as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 67733c95a1..f044c025d8 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -54,7 +54,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   | Global local ->
       let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
       let gr = Names.GlobRef.ConstRef kn in
-      let () = Declare.declare_univ_binders gr udecl in
+      let () = DeclareUniv.declare_univ_binders gr udecl in
       gr
   in
   let () = maybe_declare_manual_implicits false gr imps in
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
new file mode 100644
index 0000000000..2375028541
--- /dev/null
+++ b/vernac/declareInd.ml
@@ -0,0 +1,214 @@
+(************************************************************************)
+(*         *   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 Entries
+
+(** 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 (GlobRef.IndRef (kn,i));
+    for j=1 to List.length lc do
+      Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j));
+    done) mie.mind_entry_inds
+
+type inductive_obj = {
+  ind_names : (Id.t * Id.t list) list
+  (* For each block, name of the type + name of constructors *)
+}
+
+let inductive_names sp kn obj =
+  let (dp,_) = Libnames.repr_path sp in
+  let kn = Global.mind_of_delta_kn kn in
+  let names, _ =
+    List.fold_left
+      (fun (names, n) (typename, consnames) ->
+         let ind_p = (kn,n) in
+         let names, _ =
+           List.fold_left
+             (fun (names, p) l ->
+                let sp =
+                  Libnames.make_path dp l
+                in
+                  ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
+             (names, 1) consnames in
+         let sp = Libnames.make_path dp typename
+         in
+           ((sp, GlobRef.IndRef ind_p) :: names, n+1))
+      ([], 0) obj.ind_names
+  in names
+
+let load_inductive i ((sp, kn), names) =
+  let names = inductive_names sp kn names in
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
+
+let open_inductive i ((sp, kn), names) =
+  let names = inductive_names sp kn names in
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
+
+let cache_inductive ((sp, kn), names) =
+  let names = inductive_names sp kn names in
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp, kn), names) =
+  Some names
+
+let inInductive : inductive_obj -> Libobject.obj =
+  let open Libobject in
+  declare_object {(default_object "INDUCTIVE") with
+    cache_function = cache_inductive;
+    load_function = load_inductive;
+    open_function = open_inductive;
+    classify_function = (fun a -> Substitute a);
+    subst_function = ident_subst_function;
+    discharge_function = discharge_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) -> Libobject.obj =
+  let open Libobject in
+  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 name = Label.to_id label in
+  let univs, u = match univs with
+    | Monomorphic_entry _ ->
+      (* Global constraints already defined through the inductive *)
+      Monomorphic_entry Univ.ContextSet.empty, 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 = Declare.definition_entry ~types ~univs term in
+  let cst = Declare.declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (Declare.DefinitionEntry entry) 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
+  let open Declarations 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
+      CArray.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
+
+let feedback_axiom () = Feedback.(feedback AddedAxiom)
+
+let is_unsafe_typing_flags () =
+  let open Declarations in
+  let flags = Environ.typing_flags (Global.env()) in
+  not (flags.check_universes && flags.check_guarded && flags.check_positive)
+
+(* for initial declaration *)
+let declare_mind mie =
+  let id = match mie.mind_entry_inds with
+    | ind::_ -> ind.mind_entry_typename
+    | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
+  let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
+  let names = List.map map_names mie.mind_entry_inds in
+  List.iter (fun (typ, cons) ->
+      Declare.check_exists typ;
+      List.iter Declare.check_exists cons) names;
+  let _kn' = Global.add_mind id mie in
+  let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in
+  if is_unsafe_typing_flags() then feedback_axiom ();
+  let mind = Global.mind_of_delta_kn kn in
+  let isprim = declare_projections mie.mind_entry_universes mind in
+  Impargs.declare_mib_implicits mind;
+  declare_inductive_argument_scopes mind mie;
+  oname, isprim
+
+let is_recursive mie =
+  let open Constr in
+  let rec is_recursive_constructor lift typ =
+    match Constr.kind typ with
+    | Prod (_,arg,rest) ->
+        not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) ||
+        is_recursive_constructor (lift+1) rest
+    | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
+    | _ -> false
+  in
+  match mie.mind_entry_inds with
+  | [ind] ->
+      let nparams = List.length mie.mind_entry_params in
+      List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc
+  | _ -> false
+
+let warn_non_primitive_record =
+  CWarnings.create ~name:"non-primitive-record" ~category:"record"
+    (fun indsp ->
+       Pp.(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++
+                  strbrk" could not be defined as a primitive record")))
+
+let minductive_message = function
+  | []  -> CErrors.user_err Pp.(str "No inductive definition.")
+  | [x] -> Pp.(Id.print x ++ str " is defined")
+  | l   -> Pp.(hov 0 (prlist_with_sep pr_comma Id.print l ++
+                      spc () ++ str "are defined"))
+
+type one_inductive_impls =
+  Impargs.manual_implicits (* for inds *) *
+  Impargs.manual_implicits list (* for constrs *)
+
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
+  (* spiwack: raises an error if the structure is supposed to be non-recursive,
+        but isn't *)
+  begin match mie.mind_entry_finite with
+    | Declarations.BiFinite when is_recursive mie ->
+      if Option.has_some mie.mind_entry_record then
+        CErrors.user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
+      else
+        CErrors.user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command."))
+    | _ -> ()
+  end;
+  let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
+  let (_, kn), prim = declare_mind mie in
+  let mind = Global.mind_of_delta_kn kn in
+  if primitive_expected && not prim then warn_non_primitive_record (mind,0);
+  DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
+  List.iteri (fun i (indimpls, constrimpls) ->
+      let ind = (mind,i) in
+      let gr = GlobRef.IndRef ind in
+      Impargs.maybe_declare_manual_implicits false gr indimpls;
+      List.iteri
+        (fun j impls ->
+           Impargs.maybe_declare_manual_implicits false
+             (GlobRef.ConstructRef (ind, succ j)) impls)
+        constrimpls)
+    impls;
+  Flags.if_verbose Feedback.msg_info (minductive_message names);
+  if mie.mind_entry_private == None
+  then Indschemes.declare_default_schemes mind;
+  mind
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
new file mode 100644
index 0000000000..df8895a999
--- /dev/null
+++ b/vernac/declareInd.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** Registering a mutual inductive definition together with its
+   associated schemes *)
+
+type one_inductive_impls =
+  Impargs.manual_implicits (* for inds *) *
+  Impargs.manual_implicits list (* for constrs *)
+
+val declare_mutual_inductive_with_eliminations
+  : ?primitive_expected:bool
+  -> Entries.mutual_inductive_entry
+  -> UnivNames.universe_binders
+  -> one_inductive_impls list
+  -> Names.MutInd.t
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
new file mode 100644
index 0000000000..69ba9d76ec
--- /dev/null
+++ b/vernac/declareUniv.ml
@@ -0,0 +1,110 @@
+(************************************************************************)
+(*         *   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
+
+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_universe sp =
+  if Nametab.exists_universe sp then
+    raise (Declare.AlreadyDeclared (Some "Universe", Libnames.basename sp))
+  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_universe sp;
+  Nametab.push_universe i sp univ
+
+let cache_univ_names ((sp, _), (src, univs)) =
+  let depth = Lib.sections_depth () in
+  let dp = Libnames.pop_dirpath_n depth (Libnames.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) (Libnames.dirpath sp) src) univs
+
+let open_univ_names i ((sp, _), (src, univs)) =
+  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.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 =
+  let open Libobject in
+  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 = let open GlobRef in match gr with
+      | ConstRef c -> Label.to_id @@ Constant.label c
+      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+      | VarRef id ->
+        CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
+      | ConstructRef _ ->
+        CErrors.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 = Global.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      CErrors.user_err ~hdr:"Constraint"
+        (Pp.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 src = if poly then BoundUniv else UnqualifiedUniv in
+  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+  Declare.declare_universe_context ~poly ctx
+
+let do_constraint ~poly l =
+  let open Univ in
+  let u_of_id x =
+    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
+  in
+  let constraints = List.fold_left (fun acc (l, d, r) ->
+      let lu = u_of_id l and ru = u_of_id r in
+      Constraint.add (lu, d, ru) acc)
+      Constraint.empty l
+  in
+  let uctx = ContextSet.add_constraints constraints ContextSet.empty in
+  Declare.declare_universe_context ~poly uctx
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
new file mode 100644
index 0000000000..ce2a6e225c
--- /dev/null
+++ b/vernac/declareUniv.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*         *   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
+
+(** Global universe contexts, names and constraints *)
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
+
+val do_universe : poly:bool -> lident list -> unit
+val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e49277c51b..5ace8b917c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -335,7 +335,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
   in
   let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in
   let () = Declare.assumption_message name in
-  Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
+  DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
   (* This takes care of the implicits and hook for the current constant*)
   process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms
 
@@ -425,7 +425,7 @@ let finish_proved env sigma idopt po info =
             then Proof_using.suggest_constant (Global.env ()) kn
           in
           let gr = GlobRef.ConstRef kn in
-          Declare.declare_univ_binders gr (UState.universe_binders universes);
+          DeclareUniv.declare_univ_binders gr (UState.universe_binders universes);
           gr
       in
       Declare.definition_message name;
diff --git a/vernac/record.ml b/vernac/record.ml
index 831fb53549..b60bfdfa22 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -466,7 +466,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   in
   let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
   let impls = List.map (fun _ -> paramimpls, []) record_data in
-  let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
+  let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
       ~primitive_expected:!primitive_flag
   in
   let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index afc701edbc..956b56e256 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -13,6 +13,7 @@ Ppvernac
 Proof_using
 Egramcoq
 Metasyntax
+DeclareUniv
 DeclareDef
 DeclareObl
 Canonical
@@ -28,6 +29,7 @@ ComDefinition
 Classes
 ComPrimitive
 ComAssumption
+DeclareInd
 ComInductive
 ComFixpoint
 ComProgramFixpoint
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 430cee62c2..4ecd815dd2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -814,14 +814,14 @@ let vernac_universe ~poly l =
     user_err ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
-  Declare.do_universe ~poly l
+  DeclareUniv.do_universe ~poly l
 
 let vernac_constraint ~poly l =
   if poly && not (Global.sections_are_opened ()) then
     user_err ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
-  Declare.do_constraint ~poly l
+  DeclareUniv.do_constraint ~poly l
 
 (**********************)
 (* Modules            *)