Implement section discharging inside kernel.

This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.

7 files changed, 189 insertions, 135 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8d34f3a34f..ddaed6c941 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,9 +113,16 @@ type library_info = DirPath.t * vodigest
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
 
+(** Part of the safe_env at a section opening time to be backtracked *)
+type section_data = {
+  rev_env : Environ.env;
+  rev_univ : Univ.ContextSet.t;
+  rev_objlabels : Label.Set.t;
+}
+
 type safe_environment =
   { env : Environ.env;
-    sections : Section.t;
+    sections : section_data Section.t;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -326,12 +333,18 @@ type constraints_addition =
   | Later of Univ.ContextSet.t Future.computation
 
 let push_context_set poly cst senv =
-  let () = if Section.is_polymorphic senv.sections && not (Univ.ContextSet.is_empty cst) then
+  if Univ.ContextSet.is_empty cst then senv
+  else if Section.is_polymorphic senv.sections then
     CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.")
-  in
-  { senv with
-    env = Environ.push_context_set ~strict:(not poly) cst senv.env;
-    univ = Univ.ContextSet.union cst senv.univ }
+  else
+    let sections =
+      if Section.is_empty senv.sections then senv.sections
+      else Section.push_constraints cst senv.sections
+    in
+    { senv with
+      env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+      univ = Univ.ContextSet.union cst senv.univ;
+      sections }
 
 let add_constraints cst senv =
   match cst with
@@ -819,11 +832,10 @@ let export_private_constants ~in_section ce senv =
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_recipe ~in_section l r senv =
-  let kn = Constant.make2 senv.modpath l in
+let add_recipe ~in_section kn r senv =
   let cb = Term_typing.translate_recipe senv.env kn r in
   let senv = add_constant_aux ~in_section senv (kn, cb) in
-  kn, senv
+  senv
 
 let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
@@ -934,13 +946,68 @@ let add_module l me inl senv =
 (** {6 Interactive sections *)
 
 let open_section ~poly senv =
-  let sections = Section.open_section ~poly senv.sections in
+  let custom = {
+    rev_env = senv.env;
+    rev_univ = senv.univ;
+    rev_objlabels = senv.objlabels;
+  } in
+  let sections = Section.open_section ~poly ~custom senv.sections in
   { senv with sections }
 
 let close_section senv =
-  (* TODO: implement me when discharging in kernel *)
-  let sections = Section.close_section senv.sections in
-  { senv with sections }
+  let open Section in
+  let sections0 = senv.sections in
+  let env0 = senv.env in
+  (* First phase: revert the declarations added in the section *)
+  let sections, entries, cstrs, revert = Section.close_section sections0 in
+  let () = assert (not (Section.is_polymorphic sections0) || Univ.ContextSet.is_empty cstrs) in
+  let rec pop_revstruct accu entries revstruct = match entries, revstruct with
+  | [], revstruct -> accu, revstruct
+  | _ :: _, [] ->
+    CErrors.anomaly (Pp.str "Unmatched section data")
+  | entry :: entries, (lbl, leaf) :: revstruct ->
+    let data = match entry, leaf with
+    | SecDefinition kn, SFBconst cb ->
+      let () = assert (Label.equal lbl (Constant.label kn)) in
+      `Definition (kn, cb)
+    | SecInductive ind, SFBmind mib ->
+      let () = assert (Label.equal lbl (MutInd.label ind)) in
+      `Inductive (ind, mib)
+    | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) ->
+      CErrors.anomaly (Pp.str "Section content mismatch")
+    | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) ->
+      CErrors.anomaly (Pp.str "Module inside a section")
+    in
+    pop_revstruct (data :: accu) entries revstruct
+  in
+  let redo, revstruct = pop_revstruct [] entries senv.revstruct in
+  (* Don't revert the delayed constraints. If some delayed constraints were
+     forced inside the section, they have been turned into global monomorphic
+     that are going to be replayed. FIXME: the other ones are added twice. *)
+  let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in
+  let senv = { senv with env; revstruct; sections; univ; objlabels; } in
+  (* Second phase: replay the discharged section contents *)
+  let senv = add_constraints (Now cstrs) senv in
+  let modlist = Section.replacement_context env0 sections0 in
+  let cooking_info seg =
+    let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
+    let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in
+    { Opaqueproof.modlist; abstract }
+  in
+  let fold senv = function
+  | `Definition (kn, cb) ->
+    let in_section = not (Section.is_empty senv.sections) in
+    let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
+    let r = { Cooking.from = cb; info } in
+    add_recipe ~in_section kn r senv
+  | `Inductive (ind, mib) ->
+    let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
+    let mie = Cooking.cook_inductive info mib in
+    let mie = InferCumulativity.infer_inductive senv.env mie in
+    let _, senv = add_mind (MutInd.label ind) mie senv in
+    senv
+  in
+  List.fold_left fold senv redo
 
 (** {6 Starting / ending interactive modules and module types } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 10fedc2faf..d3ca642a89 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -27,13 +27,15 @@ val digest_match : actual:vodigest -> required:vodigest -> bool
 
 type safe_environment
 
+type section_data
+
 val empty_environment : safe_environment
 
 val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
-val sections_of_safe_env : safe_environment -> Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t
 
 (** The safe_environment state monad *)
 
@@ -89,9 +91,6 @@ val add_constant :
   side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
     (Constant.t * 'a) safe_transformer
 
-val add_recipe :
-  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
-
 (** Adding an inductive type *)
 
 val add_mind :
diff --git a/kernel/section.ml b/kernel/section.ml
index 12e9c2fd60..188249e77e 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -18,9 +18,9 @@ type _ section_kind =
 | SecMono : [ `mono ] section_kind
 | SecPoly : [ `poly ] section_kind
 
-type _ section_universes =
-| SecMonoUniv : [ `mono ] section_universes
-| SecPolyUniv : Name.t array * UContext.t -> [ `poly ] section_universes
+type (_, 'a) section_universes =
+| SecMonoUniv : 'a -> ([ `mono ], 'a) section_universes
+| SecPolyUniv : Name.t array * UContext.t -> ([ `poly ], 'a) section_universes
 
 type section_entry =
 | SecDefinition of Constant.t
@@ -28,21 +28,23 @@ type section_entry =
 
 type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
 
-type 'a section = {
+type ('a, 'b) section = {
   sec_context : int;
   (** Length of the named context suffix that has been introduced locally *)
-  sec_universes : 'a section_universes;
+  sec_universes : ('a, ContextSet.t) section_universes;
   (** Universes local to the section *)
   sec_entries : section_entry list;
   (** Definitions introduced in the section *)
-  sec_data : 'a section_universes entry_map;
+  sec_data : ('a, unit) section_universes entry_map;
+  (** Additional data synchronized with the section *)
+  sec_custom : 'b;
 }
 
 (** Sections can be nested with the proviso that no monomorphic section can be
     opened inside a polymorphic one. The reverse is allowed. *)
-type t = {
-  sec_poly : [ `poly ] section list;
-  sec_mono : [ `mono ] section list;
+type 'a t = {
+  sec_poly : ([ `poly ], 'a) section list;
+  sec_mono : ([ `mono ], 'a) section list;
 }
 
 let empty = {
@@ -64,7 +66,7 @@ let add_emap e v (cmap, imap) = match e with
 | SecDefinition con -> (Cmap.add con v cmap, imap)
 | SecInductive ind -> (cmap, Mindmap.add ind v imap)
 
-type on_sec = { on_sec : 'a. 'a section_kind -> 'a section -> 'a section }
+type 'b on_sec = { on_sec : 'a. 'a section_kind -> ('a, 'b) section -> ('a, 'b) section }
 
 let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
 | [], [] -> CErrors.user_err (Pp.str "No opened section")
@@ -75,7 +77,7 @@ let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
   let sec_mono = f.on_sec SecMono sec :: rem in
   { sec_mono; sec_poly }
 
-type 'r with_sec = { with_sec : 'a. ('a section_kind * 'a section) option -> 'r }
+type ('r, 'b) with_sec = { with_sec : 'a. ('a section_kind * ('a, 'b) section) option -> 'r }
 
 let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
 | [], [] -> f.with_sec None
@@ -87,7 +89,7 @@ let push_local s =
   on_last_section { on_sec } s
 
 let push_context (nas, ctx) s =
-  let on_sec (type a) (kind : a section_kind) (sec : a section) : a section = match kind with
+  let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with
   | SecMono ->
     CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section")
   | SecPoly ->
@@ -97,35 +99,48 @@ let push_context (nas, ctx) s =
   in
   on_last_section { on_sec } s
 
-let open_section ~poly sections =
+let push_constraints uctx s =
+  let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with
+  | SecMono ->
+    let SecMonoUniv uctx' = sec.sec_universes in
+    let sec_universes = SecMonoUniv (ContextSet.union uctx uctx') in
+    { sec with sec_universes }
+  | SecPoly ->
+    CErrors.anomaly (Pp.str "Adding monomorphic constraints to polymorphic section")
+  in
+  on_last_section { on_sec } s
+
+let open_section ~poly ~custom sections =
   if poly then
     let sec = {
       sec_context = 0;
       sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
       sec_entries = [];
       sec_data = (Cmap.empty, Mindmap.empty);
+      sec_custom = custom;
     } in
     { sections with sec_poly = sec :: sections.sec_poly }
   else if List.is_empty sections.sec_poly then
     let sec = {
       sec_context = 0;
-      sec_universes = SecMonoUniv;
+      sec_universes = SecMonoUniv Univ.ContextSet.empty;
       sec_entries = [];
       sec_data = (Cmap.empty, Mindmap.empty);
+      sec_custom = custom;
     } in
     { sections with sec_mono = sec :: sections.sec_mono }
   else
     CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
 
 let close_section sections =
-  (* TODO: implement me correctly when discharging in kernel *)
   match sections.sec_poly, sections.sec_mono with
-  | _sec :: psecs, _ ->
+  | sec :: psecs, _ ->
     let sections = { sections with sec_poly = psecs } in
-    sections
-  | [], _sec :: msecs ->
+    sections, sec.sec_entries, Univ.ContextSet.empty, sec.sec_custom
+  | [], sec :: msecs ->
     let sections = { sections with sec_mono = msecs } in
-    sections
+    let SecMonoUniv cstrs = sec.sec_universes in
+    sections, sec.sec_entries, cstrs, sec.sec_custom
   | [], [] ->
     CErrors.user_err (Pp.str "No opened section.")
 
@@ -133,13 +148,17 @@ let same_poly (type a) ~poly (knd : a section_kind) = match knd with
 | SecPoly -> poly
 | SecMono -> not poly
 
+let drop_global (type a) : (a, _) section_universes -> (a, unit) section_universes = function
+| SecMonoUniv _ -> SecMonoUniv ()
+| SecPolyUniv _ as u -> u
+
 let push_global ~poly e s =
   if is_empty s then s
   else
     let on_sec knd sec =
       if same_poly ~poly knd then { sec with
         sec_entries = e :: sec.sec_entries;
-        sec_data = add_emap e sec.sec_universes sec.sec_data;
+        sec_data = add_emap e (drop_global sec.sec_universes) sec.sec_data;
       } else
         CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
           monomorphic declarations in sections.")
@@ -179,13 +198,13 @@ let extract_hyps sec vars hyps =
 let section_segment_of_entry vars e hyps sections =
   (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
     global *)
-  let with_sec (type a) (s : (a section_kind * a section) option) = match s with
+  let with_sec (type a) (s : (a section_kind * (a, _) section) option) = match s with
   | None ->
     CErrors.user_err (Pp.str "No opened section.")
   | Some (knd, sec) ->
     let hyps = extract_hyps sec vars hyps in
     let inst, auctx = match knd, find_emap e sec.sec_data with
-    | SecMono, SecMonoUniv ->
+    | SecMono, SecMonoUniv () ->
       Instance.empty, AUContext.empty
     | SecPoly, SecPolyUniv (nas, ctx) ->
       Univ.abstract_universes nas ctx
diff --git a/kernel/section.mli b/kernel/section.mli
index 4b23115ca2..c1026a2980 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -13,39 +13,51 @@ open Univ
 
 (** Kernel implementation of sections. *)
 
-type t
-(** Type of sections *)
+type 'a t
+(** Type of sections with additional data ['a] *)
 
-val empty : t
+val empty : 'a t
 
-val is_empty : t -> bool
+val is_empty : 'a t -> bool
 (** Checks whether there is no opened section *)
 
-val is_polymorphic : t -> bool
+val is_polymorphic : 'a t -> bool
 (** Checks whether last opened section is polymorphic *)
 
 (** {6 Manipulating sections} *)
 
-val open_section : poly:bool -> t -> t
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+val open_section : poly:bool -> custom:'a -> 'a t -> 'a t
 (** Open a new section with the provided universe polymorphic status. Sections
     can be nested, with the proviso that polymorphic sections cannot appear
-    inside a monomorphic one. *)
+    inside a monomorphic one. A custom data can be attached to this section,
+    that will be returned by {!close_section}. *)
 
-val close_section : t -> t
+val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a
+(** Close the current section and returns the entries defined inside, the set
+    of global monomorphic constraints added in this section, and the custom data
+    provided at the opening of the section. *)
 
 (** {6 Extending sections} *)
 
-val push_local : t -> t
+val push_local : 'a t -> 'a t
 (** Extend the current section with a local definition (cf. push_named). *)
 
-val push_context : Name.t array * UContext.t -> t -> t
+val push_context : Name.t array * UContext.t -> 'a t -> 'a t
 (** Extend the current section with a local universe context. Assumes that the
     last opened section is polymorphic. *)
 
-val push_constant : poly:bool -> Constant.t -> t -> t
+val push_constraints : ContextSet.t -> 'a t -> 'a t
+(** Extend the current section with a global universe context.
+    Assumes that the last opened section is monomorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> 'a t -> 'a t
 (** Make the constant as having been defined in this section. *)
 
-val push_inductive : poly:bool -> MutInd.t -> t -> t
+val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
 (** Make the inductive block as having been defined in this section. *)
 
 (** {6 Retrieving section data} *)
@@ -64,15 +76,15 @@ type abstr_info = private {
 val empty_segment : abstr_info
 (** Nothing to abstract *)
 
-val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+val segment_of_constant : Environ.env -> Constant.t -> 'a t -> abstr_info
 (** Section segment at the time of the constant declaration *)
 
-val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+val segment_of_inductive : Environ.env -> MutInd.t -> 'a t -> abstr_info
 (** Section segment at the time of the inductive declaration *)
 
-val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list
 (** Section segments of all declarations from this section. *)
 
-val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool
 
-val is_polymorphic_univ : Level.t -> t -> bool
+val is_polymorphic_univ : Level.t -> 'a t -> bool
diff --git a/library/global.ml b/library/global.ml
index 3d28178d7b..315a147d2c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -71,6 +71,11 @@ let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ()))
 let globalize f =
   let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res
 
+let globalize0_with_summary fs f =
+  let env = f (safe_env ()) in
+  Summary.unfreeze_summaries fs;
+  GlobalSafeEnv.set_safe_env env
+
 let globalize_with_summary fs f =
   let res,env = f (safe_env ()) in
   Summary.unfreeze_summaries fs;
@@ -99,18 +104,13 @@ let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d)
-let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
 let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
-let close_section fs =
-  (* TODO: use globalize0_with_summary *)
-  Summary.unfreeze_summaries fs;
-  let env = Safe_typing.close_section (safe_env ()) in
-  GlobalSafeEnv.set_safe_env env
+let close_section fs = globalize0_with_summary fs Safe_typing.close_section
 
 let start_module id = globalize (Safe_typing.start_module (i2l id))
 let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
diff --git a/library/global.mli b/library/global.mli
index b809e9b241..26ccb90271 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -52,7 +52,6 @@ val export_private_constants : in_section:bool ->
 
 val add_constant :
   side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
-val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 208b8e28a7..bd47fc147e 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -70,8 +70,6 @@ let declare_universe_context ~poly ctx =
 (** 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 : Decls.logical_kind;
   cst_locl : import_status;
 }
@@ -102,12 +100,6 @@ let load_constant i ((sp,kn), obj) =
   Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con);
   Dumpglob.add_constant_kind con obj.cst_kind
 
-let cooking_info segment =
-  let modlist = replacement_context () in
-  let { abstr_ctx = named_ctx; abstr_subst = subst; abstr_uctx = uctx } = segment 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 *)
@@ -127,31 +119,20 @@ let check_exists id =
 let cache_constant ((sp,kn), obj) =
   (* Invariant: the constant must exist in the logical environment, except when
      redefining it when exiting a section. See [discharge_constant]. *)
-  let id = Libnames.basename sp in
   let kn' =
-    match obj.cst_decl with
-    | None ->
-      if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
-      then Constant.make1 kn
-      else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
-    | Some r ->
-      Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r
+    if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
+    then Constant.make1 kn
+    else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
   Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
-  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 { Cooking.from; info } }
+  Some obj
 
 (* 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;
 }
@@ -176,7 +157,6 @@ let update_tables c =
 
 let register_constant kn kind local =
   let o = inConstant {
-    cst_decl = None;
     cst_kind = kind;
     cst_locl = local;
   } in
@@ -384,12 +364,17 @@ let declare_inductive_argument_scopes kn mie =
       Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j));
     done) mie.mind_entry_inds
 
-let inductive_names sp kn mie =
+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) ind ->
+      (fun (names, n) (typename, consnames) ->
          let ind_p = (kn,n) in
          let names, _ =
            List.fold_left
@@ -398,68 +383,37 @@ let inductive_names sp kn mie =
                   Libnames.make_path dp l
                 in
                   ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
-             (names, 1) ind.mind_entry_consnames in
-         let sp = Libnames.make_path dp ind.mind_entry_typename
+             (names, 1) consnames in
+         let sp = Libnames.make_path dp typename
          in
            ((sp, GlobRef.IndRef ind_p) :: names, n+1))
-      ([], 0) mie.mind_entry_inds
+      ([], 0) obj.ind_names
   in names
 
-let load_inductive i ((sp,kn),mie) =
-  let names = inductive_names sp kn mie in
+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),mie) =
-  let names = inductive_names sp kn mie in
+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),mie) =
-  let names = inductive_names sp kn mie in
-  List.iter check_exists (List.map (fun p -> Libnames.basename (fst p)) names);
-  let id = Libnames.basename sp in
-  let kn' = Global.add_mind id mie in
-  assert (MutInd.equal kn' (MutInd.make1 kn));
+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),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 = Constr.mkProp;
-  mind_entry_template = false;
-  mind_entry_consnames = mie.mind_entry_consnames;
-  mind_entry_lc = []
-}
+let discharge_inductive ((sp, kn), names) =
+  Some names
 
-(* 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 =
+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 (dummy_inductive_entry a));
+    classify_function = (fun a -> Substitute 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
 
@@ -516,7 +470,11 @@ 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 (sp,kn as oname) = add_leaf id (inInductive mie) 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