diff --git a/interp/impargs.ml b/interp/impargs.ml
index 8d3017795367..fe11d3d00431 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -570,19 +570,24 @@ let add_section_impls vars extra_impls (cond,impls) =
   let p = List.length vars - List.length extra_impls in
   adjust_side_condition p cond, extra_impls @ List.map (Option.map (lift_implicits p)) impls
 
+let discharge_request = function
+  | ImplMutualInductive (mind,flags) -> ImplMutualInductive (Lib.discharge_mind mind, flags)
+  | ImplInteractive _ | ImplConstant _ | ImplLocal as req -> req
+
 let discharge_implicits (req,l) =
   match req with
   | ImplLocal -> None
   | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ ->
      let l' =
-       try
-         List.map (fun (gr, l) ->
-             let vars = Array.map_to_list Constr.destVar (Lib.section_instance gr) in
+       List.map (fun (gr, l) ->
+           match Lib.discharge_global_reference_with_instance gr with
+           | Some (gr,inst) ->
+             let vars = Array.map_to_list Constr.destVar inst in
              let extra_impls = impls_of_context vars in
              let newimpls = List.map (add_section_impls vars extra_impls) l in
-             (gr, newimpls)) l
-       with Not_found -> l in
-     Some (req,l')
+             (gr, newimpls)
+           | None -> assert false (* Would be ImplLocal *)) l in
+     Some (discharge_request req,l')
 
 let rebuild_implicits (req,l) =
   match req with
@@ -591,8 +596,8 @@ let rebuild_implicits (req,l) =
       let ref,oldimpls = List.hd l in
       let newimpls = compute_global_implicits flags ref in
       req, [ref, List.map2 merge_impls oldimpls newimpls]
-  | ImplMutualInductive (kn,flags) ->
-      let newimpls = compute_all_mib_implicits flags kn in
+  | ImplMutualInductive (mind,flags) ->
+      let newimpls = compute_all_mib_implicits flags mind in
       let rec aux olds news =
        match olds, news with
        | (_, oldimpls) :: old, (gr, newimpls) :: tl ->
diff --git a/interp/notation.ml b/interp/notation.ml
index fe7a4af85a6a..0bc32cbea15e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1911,13 +1911,12 @@ let discharge_available_scopes map =
       if List.is_empty ltop && List.is_empty lbot then None else Some (ltop, lbot)) map
 
 let discharge_arguments_scope (req,r,scs,_cls,available_scopes) =
-  if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
+  if req == ArgsScopeNoDischarge then None
   else
-    let n =
-      try
-        Array.length (Lib.section_instance r)
-      with
-        Not_found (* Not a ref defined in this section *) -> 0 in
+    match Lib.discharge_global_reference_with_instance r with
+    | None -> None
+    | Some (r, inst) ->
+    let n = Array.length inst in
     let available_scopes = discharge_available_scopes available_scopes in
     (* Hack: use list cls to encode an integer to pass to rebuild for Manual case *)
     (* since cls is anyway recomputed in rebuild *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b4603356ab42..922b5bdc494d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -125,11 +125,19 @@ type cooking_cache = {
   rel_ctx : rel_context Lazy.t;
 }
 
+let discharge_mind {info = {expand_info = (_csttab, mindtab);_};_} mind =
+  if Mindmap.mem mind mindtab then MutInd.pop mind else mind
+
+let discharge_inductive cache (mind,i) = (discharge_mind cache mind, i)
+
+let discharge_constant {info = {expand_info = (csttab, _mindtab);_};_} cst =
+  if Cmap.mem cst csttab then Constant.pop cst else cst
+
 let instantiate_my_gr gr u =
   match gr with
-  | ConstRef c -> mkConstU (c, u)
-  | IndRef i -> mkIndU (i, u)
-  | ConstructRef c -> mkConstructU (c, u)
+  | ConstRef c -> mkConstU (Constant.pop c, u)
+  | IndRef i -> mkIndU (Ind.pop i, u)
+  | ConstructRef c -> mkConstructU (Construct.pop c, u)
 
 let discharge_inst top_abst_subst sub_abst_rev_inst =
   let rec aux k relargs top_abst_subst sub_abst_rev_inst =
@@ -172,11 +180,11 @@ let share_univs cache top_abst_subst k r u l =
 let discharge_proj_repr r p = (* To merge with discharge_proj *)
   let nnewpars = List.count NamedDecl.is_local_assum r.abstr_info.abstr_ctx in
   let map npars = npars + nnewpars in
-  Projection.Repr.map_npars map p
+  Projection.Repr.map_npars map (Projection.Repr.pop p)
 
 let discharge_proj (_,_,abstr_inst_length) p =
   let map npars = npars + abstr_inst_length in
-  Projection.map_npars map p
+  Projection.map_npars map (Projection.pop p)
 
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
@@ -190,7 +198,7 @@ let expand_constr cache modlist top_abst_subst c =
         | (abstr_uinst, abstr_inst_rel, abstr_inst_length) ->
           let u = Instance.append abstr_uinst u in
           let pms = Array.append (make_inst k abstr_inst_rel) pms in
-          let ci = { ci with ci_npar = ci.ci_npar + abstr_inst_length } in
+          let ci = { ci with ci_npar = ci.ci_npar + abstr_inst_length; ci_ind = Ind.pop ci.ci_ind } in
           Constr.map_with_binders succ substrec k (mkCase (ci,u,pms,p,iv,t,br))
         | exception Not_found ->
           Constr.map_with_binders succ substrec k c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index efc54106adcb..1d0903bd81da 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -58,6 +58,9 @@ val create_cache : cooking_info -> cooking_cache
 val instance_of_cooking_cache : cooking_cache -> Constr.t array
 val rel_context_of_cooking_cache : cooking_cache -> rel_context
 
+val discharge_inductive : cooking_cache -> Ind.t -> Ind.t
+val discharge_constant : cooking_cache -> Constant.t -> Constant.t
+
 val abstract_as_type : cooking_cache -> types -> types
 
 val abstract_as_body : cooking_cache -> constr -> constr
diff --git a/kernel/discharge.ml b/kernel/discharge.ml
index 297a1666037a..86b6aa8d6b86 100644
--- a/kernel/discharge.ml
+++ b/kernel/discharge.ml
@@ -111,6 +111,15 @@ let cook_projection cache ~params t =
   let _, t = decompose_prod_n_decls (Context.Rel.length params + 1 + nrels) t in
   t
 
+let cook_nested_type cache = function
+  | NestedInd ind -> NestedInd (Cooking.discharge_inductive cache ind)
+  | NestedPrimitive cst -> NestedPrimitive (Cooking.discharge_constant cache cst)
+
+let cook_recargs cache = function
+  | Mrec ind -> Mrec (Ind.pop ind)
+  | Norec -> Norec
+  | Nested t -> Nested (cook_nested_type cache t)
+
 let cook_one_ind cache ~ntypes mip =
   let mind_arity = match mip.mind_arity with
     | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
@@ -139,7 +148,7 @@ let cook_one_ind cache ~ntypes mip =
     mind_nf_lc;
     mind_consnrealargs = mip.mind_consnrealargs;
     mind_consnrealdecls = mip.mind_consnrealdecls;
-    mind_recargs = mip.mind_recargs;
+    mind_recargs = Rtree.Smart.map (cook_recargs cache) mip.mind_recargs;
     mind_relevance = mip.mind_relevance;
     mind_nb_constant = mip.mind_nb_constant;
     mind_nb_args = mip.mind_nb_args;
diff --git a/kernel/names.ml b/kernel/names.ml
index 14ebce13b868..c4d794843869 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -381,6 +381,12 @@ module KerName = struct
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
+  let pop kn =
+    let mp = match kn.modpath with
+    | ModPath.MPdot (mp,_) -> mp
+    | _ -> CErrors.anomaly (str "No field to pop.") in
+    make mp kn.knlabel
+
   let to_string_gen mp_to_string kn =
     mp_to_string kn.modpath ^ "." ^ Label.to_string kn.knlabel
 
@@ -514,6 +520,10 @@ module KerPair = struct
       if mp1 == mp2 then same kn
       else make kn (KerName.make mp2 lbl)
 
+  let pop = function
+    | Same kn -> Same (KerName.pop kn)
+    | Dual (knu,knc) -> Dual (KerName.pop knu, KerName.pop knc)
+
   let to_string kp = KerName.to_string (user kp)
   let print kp = str (to_string kp)
 
@@ -625,6 +635,8 @@ struct
                                     BEWARE: indexing starts from 0. *)
   let modpath (mind, _) = MutInd.modpath mind
 
+  let pop (mind,i) = (MutInd.pop mind, i)
+
   module CanOrd =
   struct
     type nonrec t = t
@@ -673,6 +685,8 @@ struct
 
   let modpath (ind, _) = Ind.modpath ind
 
+  let pop (ind,i) = (Ind.pop ind, i)
+
   module CanOrd =
   struct
     type nonrec t = t
@@ -853,6 +867,8 @@ struct
 
     let relevant c = c.proj_relevant
 
+    let pop p = { p with proj_ind = Ind.pop p.proj_ind }
+
     let hash p =
       Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
 
@@ -960,6 +976,7 @@ struct
   let repr = fst
   let unfolded = snd
   let unfold (c, b as p) = if b then p else (c, true)
+  let pop (p,b) = (Repr.pop p, b)
 
   let equal (c, b) (c', b') = Repr.equal c c' && b == b'
 
diff --git a/kernel/names.mli b/kernel/names.mli
index b4d74190379e..f2d951d4eccf 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -291,6 +291,9 @@ sig
   val modpath : t -> ModPath.t
   val label : t -> Label.t
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   val to_string : t -> string
   (** Encode as a string (not to be used for user-facing messages). *)
 
@@ -395,6 +398,9 @@ sig
   val label : t -> Label.t
   (** Shortcut for [KerName.label (user ...)] *)
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   (** Comparisons *)
 
   include QNameS with type t := t
@@ -466,6 +472,9 @@ sig
   val label : t -> Label.t
   (** Shortcut for [KerName.label (user ...)] *)
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   (** Comparisons *)
 
   include QNameS with type t := t
@@ -504,6 +513,9 @@ sig
                                     BEWARE: indexing starts from 0. *)
   val modpath : t -> ModPath.t
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   include QNameS with type t := t
 
 end
@@ -519,6 +531,9 @@ sig
 
   val modpath : t -> ModPath.t
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   include QNameS with type t := t
 
 end
@@ -632,6 +647,7 @@ module Projection : sig
     val arg : t -> int
     val label : t -> Label.t
     val relevant : t -> bool
+    val pop : t -> t
 
     val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"]
     val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"]
@@ -662,6 +678,7 @@ module Projection : sig
   val label : t -> Label.t
   val unfolded : t -> bool
   val unfold : t -> t
+  val pop : t -> t
 
   val equal : t -> t -> bool
   [@@ocaml.deprecated "Use QProjection.equal"]
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a9a7f62ef021..487db93da5bb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -128,9 +128,7 @@ type reimport = compiled_library * Univ.ContextSet.t * vodigest
 type section_data = {
   rev_env : Environ.env;
   rev_univ : Univ.ContextSet.t;
-  rev_objlabels : Label.Set.t;
   rev_reimport : reimport list;
-  rev_revstruct : structure_body;
 }
 
 module HandleMap = Opaqueproof.HandleMap
@@ -155,6 +153,7 @@ type safe_environment =
   { env : Environ.env;
     sections : section_data Section.t option;
     modpath : ModPath.t;
+    secpath : Label.t list;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
     paramresolver : Mod_subst.delta_resolver;
@@ -184,6 +183,7 @@ let rec library_dp_of_senv senv =
 let empty_environment =
   { env = Environ.empty_env;
     modpath = ModPath.dummy;
+    secpath = [];
     modvariant = NONE;
     modresolver = Mod_subst.empty_delta_resolver;
     paramresolver = Mod_subst.empty_delta_resolver;
@@ -549,6 +549,74 @@ let add_retroknowledge pttc senv =
     env = Primred.add_retroknowledge senv.env pttc;
     local_retroknowledge = pttc::senv.local_retroknowledge }
 
+let constant_drop_section_path con =
+  let kn = Constant.user con in
+  assert (KerName.equal kn (Constant.canonical con));
+  let mp,l = KerName.repr kn in
+  let mp = match mp with
+    | MPdot (mp,_) -> mp
+    | _ -> assert false in
+  Constant.make2 mp l
+
+let mind_drop_section_path mind =
+  let kn = MutInd.user mind in
+  assert (KerName.equal kn (MutInd.canonical mind));
+  let mp,l = KerName.repr kn in
+  let mp = match mp with
+    | MPdot (mp,_) -> mp
+    | _ -> assert false in
+  MutInd.make2 mp l
+
+let add_minds =
+  List.fold_right (fun (mind,mib) -> Environ.add_mind mind mib)
+
+let rec add_inductive_previous_sections ~nohash mind mib sections =
+  let mib = if Option.has_some sections || nohash then mib else Declareops.hcons_mind mib in
+  match sections with
+  | None ->
+    ([mind, if nohash then mib else Declareops.hcons_mind mib], mib), sections
+  | Some sections ->
+    let poly = Declareops.inductive_is_polymorphic mib in
+    let sections = Section.(push_global ~poly (SecInductive mind) mib.mind_hyps sections) in
+    let info = Section.segment_of_inductive mind sections in
+    let mind' = mind_drop_section_path mind in
+    let mib' = Discharge.cook_inductive info mib in
+    let (miblist, exported_mib), sections =
+      Section.on_previous_section (add_inductive_previous_sections ~nohash mind' mib') sections in
+    let sections = Section.map_custom (fun sec ->
+        { sec with rev_env = add_minds miblist sec.rev_env }) sections in
+    ((mind,mib) :: miblist, exported_mib), Some sections
+
+let add_inductive_all_sections ~nohash env sections mind mib =
+  let (miblist, exported_mib), sections = add_inductive_previous_sections ~nohash mind mib sections in
+  let env = add_minds miblist env in
+  env, SFBmind exported_mib, sections
+
+let add_constants =
+  List.fold_right (fun (con,cb) -> Environ.add_constant con cb)
+
+let rec add_constant_previous_sections ~nohash env con cb sections =
+  match sections with
+  | None ->
+    (* This is the only place where we hashcons the contents of a constant body *)
+    ([con, if nohash then cb else Declareops.hcons_const_body cb], cb), sections
+  | Some sections ->
+    let poly = Declareops.constant_is_polymorphic cb in
+    let sections = Section.(push_global ~poly (SecDefinition con) cb.const_hyps sections) in
+    let info = Section.segment_of_constant con sections in
+    let con' = constant_drop_section_path con in
+    let cb' = Discharge.cook_constant env info cb in
+    let (cblist, exported_cb), sections =
+      Section.on_previous_section (add_constant_previous_sections ~nohash env con' cb') sections in
+    let sections = Section.map_custom (fun sec ->
+        { sec with rev_env = add_constants cblist sec.rev_env }) sections in
+    ((con, cb) :: cblist, exported_cb), Some sections
+
+let add_constant_all_sections ~nohash env sections con cb =
+  let (cblist, exported_cb), sections = add_constant_previous_sections ~nohash env con cb sections in
+  let env = add_constants cblist env in
+  env, SFBconst exported_cb, sections
+
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
 
@@ -558,7 +626,7 @@ type generic_name =
   | M (** name already known, cf the mod_mp field *)
   | MT (** name already known, cf the mod_mp field *)
 
-let add_field ((l,sfb) as field) gn senv =
+let add_field ?(nohash=false) (l,sfb) gn senv =
   let mlabs,olabs = match sfb with
     | SFBmind mib ->
       let l = labels_of_mib mib in
@@ -568,30 +636,18 @@ let add_field ((l,sfb) as field) gn senv =
     | SFBmodule _ | SFBmodtype _ ->
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
-  let env' = match sfb, gn with
-    | SFBconst cb, C con -> Environ.add_constant con cb senv.env
-    | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
-    | SFBmodtype mtb, MT -> Environ.add_modtype mtb senv.env
-    | SFBmodule mb, M -> Modops.add_module mb senv.env
+  let env', exported, sections =
+    match sfb, gn with
+    | SFBconst cb, C con -> add_constant_all_sections ~nohash senv.env senv.sections con cb
+    | SFBmind mib, I mind -> add_inductive_all_sections ~nohash senv.env senv.sections mind mib
+    | SFBmodtype mtb, MT -> Environ.add_modtype mtb senv.env, sfb, senv.sections
+    | SFBmodule mb, M -> Modops.add_module mb senv.env, sfb, senv.sections
     | _ -> assert false
   in
-  let sections = match senv.sections with
-    | None -> None
-    | Some sections ->
-      match sfb, gn with
-      | SFBconst cb, C con ->
-        let poly = Declareops.constant_is_polymorphic cb in
-        Some Section.(push_global ~poly env' (SecDefinition con) sections)
-      | SFBmind mib, I mind ->
-        let poly = Declareops.inductive_is_polymorphic mib in
-        Some Section.(push_global ~poly env' (SecInductive mind) sections)
-      | _, (M | MT) -> Some sections
-      | _ -> assert false
-  in
   { senv with
     env = env';
     sections;
-    revstruct = field :: senv.revstruct;
+    revstruct = (l,exported) :: senv.revstruct;
     modlabels = Label.Set.union mlabs senv.modlabels;
     objlabels = Label.Set.union olabs senv.objlabels }
 
@@ -621,8 +677,6 @@ let repr_exported_opaque o =
 
 let add_constant_aux senv (kn, cb) =
   let l = Constant.label kn in
-  (* This is the only place where we hashcons the contents of a constant body *)
-  let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -789,8 +843,8 @@ let export_side_effects senv eff =
   let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
   let trusted = check_signatures senv signatures in
   let push_seff env eff =
-    let { seff_constant = kn; seff_body = cb ; _ } = eff in
-    let env = Environ.add_constant kn (lift_constant cb) env in
+    let { seff_constant = con; seff_body = cb ; _ } = eff in
+    let env, _, _ (* ?? *) = add_constant_all_sections ~nohash:true env senv.sections con (lift_constant cb) in
     env
   in
   match trusted with
@@ -849,8 +903,11 @@ let export_private_constants eff senv =
   let senv = List.fold_left fold senv bodies in
   exported, senv
 
+let make_constant_in_section (mp,sec,l) =
+  Constant.make2 (List.fold_right (fun s m -> MPdot (m,s)) sec mp) l
+
 let add_constant l decl senv =
-  let kn = Constant.make2 senv.modpath l in
+  let kn = make_constant_in_section (senv.modpath,senv.secpath,l) in
   let senv, cb =
     let sec_univs = Option.map Section.all_poly_univs senv.sections in
       match decl with
@@ -942,7 +999,7 @@ let check_constraints uctx = function
 | Entries.Monomorphic_entry -> true
 
 let add_private_constant l uctx decl senv : (Constant.t * private_constants) * safe_environment =
-  let kn = Constant.make2 senv.modpath l in
+  let kn = make_constant_in_section (senv.modpath,senv.secpath,l) in
   let senv = push_context_set ~strict:true uctx senv in
     let cb =
       let sec_univs = Option.map Section.all_poly_univs senv.sections in
@@ -988,14 +1045,14 @@ let check_mind mie lab =
     assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
 
 let add_checked_mind kn mib senv =
-  let mib =
-    match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
-  in
   add_field (MutInd.label kn,SFBmind mib) (I kn) senv
 
+let make_inductive_in_section (mp,sec,l) =
+  MutInd.make2 (List.fold_right (fun s m -> MPdot (m,s)) sec mp) l
+
 let add_mind l mie senv =
   let () = check_mind mie l in
-  let kn = MutInd.make2 senv.modpath l in
+  let kn = make_inductive_in_section (senv.modpath,senv.secpath,l) in
   let sec_univs = Option.map Section.all_poly_univs senv.sections in
   let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in
   (* We still have to add the template monomorphic constraints, and only those
@@ -1057,6 +1114,7 @@ let start_mod_modtype ~istype l senv =
   {
     (* modified fields *)
     modpath = mp;
+    secpath = [];
     modvariant = if istype then SIG ([], senv) else STRUCT ([],senv);
 
     (* carried over fields *)
@@ -1249,7 +1307,7 @@ let add_include me is_module inl senv =
       | SFBmodule _ -> M
       | SFBmodtype _ -> MT
     in
-    add_field field new_name senv
+    add_field ~nohash:true field new_name senv
   in
   resolver, List.fold_left add senv str
 
@@ -1274,6 +1332,7 @@ let start_library dir senv =
   mp,
   { env = senv.env;
     modpath = mp;
+    secpath = [];
     modvariant = LIBRARY;
     required = senv.required;
 
@@ -1352,51 +1411,31 @@ let import lib cst vodigest senv =
 
 (** {6 Interactive sections *)
 
-let open_section senv =
+let open_section id senv =
   let custom = {
     rev_env = senv.env;
     rev_univ = senv.univ;
-    rev_objlabels = senv.objlabels;
     rev_reimport = [];
-    rev_revstruct = senv.revstruct;
   } in
   let sections = Section.open_section ~custom senv.sections in
-  { senv with sections=Some sections }
+  { senv with sections = Some sections; secpath = Label.of_id id :: senv.secpath }
 
 let close_section senv =
-  let open Section in
   let sections0 = get_section 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 sections, cstrs, revert = Section.close_section sections0 in
   (* Don't revert the delayed constraints (future_cst). If some delayed constraints
      were forced inside the section, they have been turned into global monomorphic
      that are going to be replayed. Those that are not forced are not readded
      by {!add_constant_aux}. *)
-  let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels;
-        rev_reimport; rev_revstruct = revstruct } = revert in
-  let senv = { senv with env; revstruct; sections; univ; objlabels; } in
+  let { rev_env = env; rev_univ = univ; rev_reimport } = revert in
+  let senv = { senv with env; sections; univ; secpath = List.tl senv.secpath } in
   (* Second phase: replay Requires *)
   let senv = List.fold_left (fun senv (lib,cst,vodigest) -> snd (import lib cst vodigest senv))
       senv (List.rev rev_reimport)
   in
-  (* Third phase: replay the discharged section contents *)
-  let senv = push_context_set ~strict:true cstrs senv in
-  let fold entry senv =
-    match entry with
-  | SecDefinition kn ->
-    let cb = Environ.lookup_constant kn env0 in
-    let info = Section.segment_of_constant kn sections0 in
-    let cb = Discharge.cook_constant senv.env info cb in
-    (* Delayed constants are already in the global environment *)
-    add_constant_aux senv (kn, cb)
-  | SecInductive ind ->
-    let mib = Environ.lookup_mind ind env0 in
-    let info = Section.segment_of_inductive ind sections0 in
-    let mib = Discharge.cook_inductive info mib in
-    add_checked_mind ind mib senv
-  in
-  List.fold_right fold entries senv
+  (* Third phase: universes *)
+  push_context_set ~strict:true cstrs senv
 
 let flatten_env senv =
   let label = function MPdot (_,l) -> l | _ -> assert false in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index dddd72c364ba..99fa90d92f4b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -168,7 +168,7 @@ val set_allow_sprop : bool -> safe_transformer0
 
 (** {6 Interactive section functions } *)
 
-val open_section : safe_transformer0
+val open_section : Id.t -> safe_transformer0
 
 val close_section : safe_transformer0
 
diff --git a/kernel/section.ml b/kernel/section.ml
index d9c6f9a360fd..b354aa84a00e 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -22,8 +22,6 @@ type section_entry =
 type 'a t = {
   prev : 'a t option;
   (** Section surrounding the current one *)
-  entries : section_entry list;
-  (** Global declarations introduced in the section *)
   context : Constr.named_context;
   (** Declarations local to the section, intended to be interleaved
       with global declarations *)
@@ -42,7 +40,9 @@ type 'a t = {
   custom : 'a;
 }
 
-let rec depth sec = 1 + match sec.prev with None -> 0 | Some prev -> depth prev
+let rec depth = function
+  | None -> 0
+  | Some sec -> 1 + depth sec.prev
 
 let has_poly_univs sec = sec.has_poly_univs
 
@@ -77,7 +77,7 @@ let push_constraints uctx sec =
   then CErrors.user_err
       Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
   let uctx' = sec.mono_universes in
-  let mono_universes =  (ContextSet.union uctx uctx') in
+  let mono_universes = ContextSet.union uctx uctx' in
   { sec with mono_universes }
 
 let open_section ~custom prev =
@@ -88,14 +88,17 @@ let open_section ~custom prev =
     poly_universes = UContext.empty;
     all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] prev;
     has_poly_univs = Option.cata has_poly_univs false prev;
-    entries = [];
     expand_info_map = (Cmap.empty, Mindmap.empty);
     cooking_info_map = (Cmap.empty, Mindmap.empty);
     custom = custom;
   }
 
 let close_section sec =
-  sec.prev, sec.entries, sec.mono_universes, sec.custom
+  sec.prev, sec.mono_universes, sec.custom
+
+let on_previous_section f sec =
+  let e, prev = f sec.prev in
+  e, { sec with prev }
 
 let push_local d sec =
   { sec with context = d :: sec.context }
@@ -104,11 +107,7 @@ let extract_hyps vars used =
   (* Only keep the part that is used by the declaration *)
   List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
 
-let segment_of_entry env e uctx sec =
-  let hyps = match e with
-  | SecDefinition con -> (Environ.lookup_constant con env).Declarations.const_hyps
-  | SecInductive mind -> (Environ.lookup_mind mind env).Declarations.mind_hyps
-  in
+let segment_of_entry e hyps uctx sec =
   let hyps = Context.Named.to_vars hyps in
   (* [sec.context] are the named hypotheses, [hyps] the subset that is
      declared by the global *)
@@ -121,19 +120,22 @@ let segment_of_entry env e uctx sec =
   in
   Cooking.make_cooking_info ~recursive sec.expand_info_map ctx uctx
 
-let push_global env ~poly e sec =
+let push_global ~poly e hyps sec =
   if has_poly_univs sec && not poly
   then CErrors.user_err
       Pp.(str "Cannot add a universe monomorphic declaration when \
                section polymorphic universes are present.")
   else
-    let cooking_info, abstr_inst_info = segment_of_entry env e sec.poly_universes sec in
+    let cooking_info, abstr_inst_info = segment_of_entry e hyps sec.poly_universes sec in
     let cooking_info_map = add_emap e cooking_info sec.cooking_info_map in
     let expand_info_map = add_emap e abstr_inst_info sec.expand_info_map in
-    { sec with entries = e :: sec.entries; expand_info_map; cooking_info_map }
+    { sec with expand_info_map; cooking_info_map }
+
+let segment_of_constant con sec =
+  Cmap.find con (fst sec.cooking_info_map)
 
-let segment_of_constant con sec = Cmap.find con (fst sec.cooking_info_map)
-let segment_of_inductive con sec = Mindmap.find con (snd sec.cooking_info_map)
+let segment_of_inductive mind sec =
+  Mindmap.find mind (snd sec.cooking_info_map)
 
 let is_in_section _env gr sec =
   let open GlobRef in
diff --git a/kernel/section.mli b/kernel/section.mli
index 1efe157af849..a779bf12a380 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -17,7 +17,7 @@ open Cooking
 type 'a t
 (** Type of sections with additional data ['a] *)
 
-val depth : 'a t -> int
+val depth : 'a t option -> int
 (** Number of nested sections. *)
 
 val map_custom : ('a -> 'a) -> 'a t -> 'a t
@@ -35,11 +35,14 @@ val open_section : custom:'a -> 'a t option -> 'a t
     inside a monomorphic one. A custom data can be attached to this section,
     that will be returned by {!close_section}. *)
 
-val close_section : 'a t -> 'a t option * section_entry list * ContextSet.t * 'a
+val close_section : 'a t -> 'a t option * 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. *)
 
+val on_previous_section : ('a t option -> 'b * 'a t option) -> 'a t -> 'b * 'a t
+(** Apply an action on the prev segment of the section *)
+
 (** {6 Extending sections} *)
 
 val push_local : Constr.named_declaration -> 'a t -> 'a t
@@ -53,7 +56,7 @@ 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_global : Environ.env -> poly:bool -> section_entry -> 'a t -> 'a t
+val push_global : poly:bool -> section_entry -> Constr.named_context -> 'a t -> 'a t
 (** Push a global entry in this section. *)
 
 (** {6 Retrieving section data} *)
diff --git a/library/coqlib.ml b/library/coqlib.ml
index dd5caef5b916..79869d0bf3f9 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -64,6 +64,11 @@ let add_ref s c =
 let cache_ref (s,c) =
   add_ref s c
 
+let discharge_ref (s,gr) =
+  match Lib.discharge_global_reference gr with
+  | None -> None
+  | Some gr -> Some (s,gr)
+
 let (inCoqlibRef : string * GlobRef.t -> Libobject.obj) =
   let open Libobject in
   declare_object { (default_object "COQLIBREF") with
@@ -71,7 +76,7 @@ let (inCoqlibRef : string * GlobRef.t -> Libobject.obj) =
     load_function = (fun _ x -> cache_ref x);
     classify_function = (fun _ -> Substitute);
     subst_function = ident_subst_function;
-    discharge_function = (fun sc -> Some sc); }
+    discharge_function = discharge_ref; }
 
 (** Replaces a binding ! *)
 let register_ref s c =
diff --git a/library/global.ml b/library/global.ml
index 6a45bb45cdfe..00265456c334 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -99,7 +99,7 @@ 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 () = globalize0 Safe_typing.open_section
+let open_section id = globalize0 (Safe_typing.open_section id)
 let close_section fs = globalize0_with_summary fs Safe_typing.close_section
 let sections_are_opened () = Safe_typing.sections_are_opened (safe_env())
 
diff --git a/library/global.mli b/library/global.mli
index 01b323810a97..15b94768d050 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -77,7 +77,7 @@ val add_include :
 
 (** Sections *)
 
-val open_section : unit -> unit
+val open_section : Id.t -> unit
 (** [poly] is true when the section should be universe polymorphic *)
 
 val close_section : Summary.Interp.frozen -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index 8c5fcbf4a47f..60ff2baf3241 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -53,6 +53,12 @@ let canonical_gr = function
   | ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j)
   | VarRef id -> VarRef id
 
+let pop_global_reference = function
+  | ConstRef cst -> ConstRef (Constant.pop cst)
+  | IndRef ind -> IndRef (Ind.pop ind)
+  | ConstructRef cstr -> ConstructRef (Construct.pop cstr)
+  | VarRef id -> VarRef id
+
 (* Extended global references *)
 
 type abbreviation = KerName.t
diff --git a/library/globnames.mli b/library/globnames.mli
index 020508008d08..bea97c25c37c 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -27,6 +27,9 @@ val destConstructRef : GlobRef.t -> constructor
 val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
+(** Remove the last modpath segment *)
+val pop_global_reference : GlobRef.t -> GlobRef.t
+
 (** {6 Extended global references } *)
 
 type abbreviation = KerName.t
diff --git a/library/lib.ml b/library/lib.ml
index 00f26763b4cc..938361a0559c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -221,12 +221,17 @@ let recalc_path_prefix () =
   in
   synterp_state := { !synterp_state with path_prefix }
 
+let pop_modpath = function
+  | MPdot (mp, _) -> mp
+  | _ -> assert false
+
 let pop_path_prefix () =
   let op = !synterp_state.path_prefix in
   synterp_state := {
     !synterp_state
     with path_prefix = Nametab.{
-        op with obj_dir = Libnames.pop_dirpath op.obj_dir;
+        obj_dir = Libnames.pop_dirpath op.obj_dir;
+        obj_mp = pop_modpath op.obj_mp;
       } }
 
 (* Modules. *)
@@ -285,6 +290,27 @@ let is_in_section ref = match sections () with
 let section_instance ref =
   Cooking.instance_of_cooking_info (section_segment_of_reference ref)
 
+let discharge_mind mind =
+  if is_in_section (IndRef (mind,0)) then MutInd.pop mind else mind
+
+let discharge_inductive ind =
+  if is_in_section (IndRef ind) then Ind.pop ind else ind
+
+let discharge_constant cst =
+  if is_in_section (ConstRef cst) then Constant.pop cst else cst
+
+let discharge_global_reference ref =
+  if is_in_section ref then
+    if Globnames.isVarRef ref then None
+    else Some (Globnames.pop_global_reference ref)
+  else Some ref
+
+let discharge_global_reference_with_instance ref =
+  if is_in_section ref then
+    if Globnames.isVarRef ref then None
+    else Some (Globnames.pop_global_reference ref, section_instance ref)
+  else Some (ref, [||])
+
 let discharge_item = Libobject.(function
   | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
   | ExportObject _ -> None
@@ -400,7 +426,8 @@ module SynterpActions : LibActions with type summary = Summary.Synterp.frozen =
   let open_section id =
     let opp = !synterp_state.path_prefix in
     let obj_dir = Libnames.add_dirpath_suffix opp.Nametab.obj_dir id in
-    let prefix = Nametab.{ obj_dir; obj_mp=opp.obj_mp; } in
+    let obj_mp = MPdot (opp.Nametab.obj_mp, Label.of_id id) in
+    let prefix = Nametab.{ obj_dir; obj_mp; } in
     check_section_fresh obj_dir id;
     let fs = Summary.Synterp.freeze_summaries () in
     add_entry (OpenedSection (prefix, fs));
@@ -471,7 +498,7 @@ module InterpActions : LibActions with type summary = Summary.Interp.frozen = st
     interp_state := stk
 
   let open_section id =
-    Global.open_section ();
+    Global.open_section id;
     let prefix = !synterp_state.path_prefix in
     let fs = Summary.Interp.freeze_summaries () in
     add_entry (OpenedSection (prefix, fs))
diff --git a/library/lib.mli b/library/lib.mli
index 1a9e45e9644f..b3e01570dc72 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -171,6 +171,12 @@ val section_segment_of_reference : GlobRef.t -> Cooking.cooking_info
 val section_instance : GlobRef.t -> Constr.t array
 val is_in_section : GlobRef.t -> bool
 
+val discharge_mind : MutInd.t -> MutInd.t
+val discharge_inductive : Ind.t -> Ind.t
+val discharge_constant : Constant.t -> Constant.t
+val discharge_global_reference : GlobRef.t -> GlobRef.t option
+val discharge_global_reference_with_instance : GlobRef.t -> (GlobRef.t * Constr.t array) option
+
 (** {6 Discharge: decrease the section level if in the current section } *)
 
 val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5707dab96435..67bfa1462320 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -207,7 +207,19 @@ let subst_Function (subst, finfos) =
     ; sprop_lemma = sprop_lemma'
     ; is_general = finfos.is_general }
 
-let discharge_Function finfos = Some finfos
+let discharge_Function finfos =
+  Some {
+    function_constant = Lib.discharge_constant finfos.function_constant;
+    graph_ind = Lib.discharge_inductive finfos.graph_ind;
+    equation_lemma = Option.map Lib.discharge_constant finfos.equation_lemma;
+    correctness_lemma =  Option.map Lib.discharge_constant finfos.correctness_lemma;
+    completeness_lemma =  Option.map Lib.discharge_constant finfos.completeness_lemma;
+    rect_lemma =  Option.map Lib.discharge_constant finfos.rect_lemma;
+    rec_lemma =  Option.map Lib.discharge_constant finfos.rec_lemma;
+    prop_lemma =  Option.map Lib.discharge_constant finfos.prop_lemma;
+    sprop_lemma =  Option.map Lib.discharge_constant finfos.sprop_lemma;
+    is_general = finfos.is_general
+  }
 
 let pr_ocst env sigma c =
   Option.fold_right
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 8e8300cb8ae8..1686a75439c7 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -42,13 +42,14 @@ let subst_rename_args (subst, (_, (r, names as orig))) =
   if r==r' then orig else (r', names)
 
 let discharge_rename_args = function
-  | ReqGlobal (c, names), _ as req when not (isVarRef c && Lib.is_in_section c) ->
-     (try
-       let var_names = Array.map_to_list (fun c -> Name (destVar c)) (Lib.section_instance c) in
+  | ReqLocal, _ -> None
+  | ReqGlobal (c, names), _ ->
+    match Lib.discharge_global_reference_with_instance c with
+    | None -> None
+    | Some (c, inst) ->
+       let var_names = Array.map_to_list (fun c -> Name (destVar c)) inst in
        let names' = var_names @ names in
        Some (ReqGlobal (c, names), (c, names'))
-     with Not_found -> Some req)
-  | _ -> None
 
 let rebuild_rename_args x = x
 
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 4ef24725ef79..d4b293d3ee3b 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -39,6 +39,12 @@ let cl_typ_ord t1 t2 = match t1, t2 with
 
 let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
 
+let discharge_coercion_class = function
+  | CL_SORT | CL_FUN | CL_SECVAR _ as x -> x
+  | CL_CONST cst -> CL_CONST (Lib.discharge_constant cst)
+  | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
+  | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p)
+
 module ClTyp = struct
   type t = cl_typ
   let compare = cl_typ_ord
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index a65d7b806719..669ddd811bd1 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -31,6 +31,8 @@ val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
 (** Comparison of [cl_typ] *)
 val cl_typ_ord : cl_typ -> cl_typ -> int
 
+val discharge_coercion_class : cl_typ -> cl_typ
+
 (** This is the type of coercion kinds *)
 type coe_typ = GlobRef.t
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fbb720b1c30c..02c6f465a8a9 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -123,17 +123,12 @@ module ReductionBehaviour = struct
     let r' = subst_global_reference subst r in if r==r' then orig
     else (local,(r',o))
 
-  let discharge = function
-    | false, (gr, b) ->
-      let b =
-        if Lib.is_in_section gr then
-          let vars = Lib.section_instance gr in
-          let extra = Array.length vars in
-          more_args extra b
-        else b
-      in
+  let discharge (local, (gr, b)) =
+    match Lib.discharge_global_reference_with_instance gr with
+    | Some (gr,inst) when not local ->
+      let b = more_args (Array.length inst) b in
       Some (false, (gr, b))
-    | true, _ -> None
+    | _ -> None
 
   let rebuild = function
     | req, (GlobRef.ConstRef c, _ as x) -> req, x
diff --git a/pretyping/structures.ml b/pretyping/structures.ml
index d72749617f86..a1d0105a11ed 100644
--- a/pretyping/structures.ml
+++ b/pretyping/structures.ml
@@ -80,6 +80,15 @@ let subst subst ({ name; projections; nparams } as s) =
   then s
   else { name; projections; nparams }
 
+let discharge_projection projs =
+  { projs with proj_body = Option.map Lib.discharge_constant projs.proj_body }
+
+let discharge { name; projections; nparams } =
+  Some
+    { name = Lib.discharge_inductive name;
+      projections = List.map discharge_projection projections;
+      nparams }
+
 let rebuild env s =
   let mib = Environ.lookup_mind (fst s.name) env in
   let nparams = mib.Declarations.mind_nparams in
@@ -325,6 +334,11 @@ let register ~warn env sigma o =
           warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
       )
 
+let discharge (ref,ind) =
+  match Lib.discharge_global_reference ref with
+  | None -> None
+  | Some ref -> Some (ref, Lib.discharge_inductive ind)
+
 end
 
 (** The canonical solution of a problem (proj,val) is a global
diff --git a/pretyping/structures.mli b/pretyping/structures.mli
index c068dffd53f7..b1a59fb5525e 100644
--- a/pretyping/structures.mli
+++ b/pretyping/structures.mli
@@ -32,6 +32,8 @@ val make : Environ.env -> Names.inductive -> projection list -> t
 val register : t -> unit
 val subst : Mod_subst.substitution -> t -> t
 
+val discharge : t -> t option
+
 (** refreshes nparams, e.g. after section discharging *)
 val rebuild : Environ.env -> t -> t
 
@@ -72,6 +74,8 @@ val register : warn:bool -> Environ.env -> Evd.evar_map -> t -> unit
 val subst : Mod_subst.substitution -> t -> t
 val repr : t -> Names.GlobRef.t
 
+val discharge : t -> t option
+
 end
 
 
diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml
index 1249ff8058d6..284f569c1177 100644
--- a/tactics/declareScheme.ml
+++ b/tactics/declareScheme.ml
@@ -27,7 +27,7 @@ let subst_scheme (subst,(kind,l)) =
   (kind, CArray.Smart.map (subst_one_scheme subst) l)
 
 let discharge_scheme (kind,l) =
-  Some (kind, l)
+  Some (kind, Array.map (fun (c,i) -> (Lib.discharge_inductive c, Lib.discharge_constant i)) l)
 
 let inScheme : string * (inductive * Constant.t) array -> Libobject.obj =
   let open Libobject in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 495ed072213a..dc74439255e3 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1237,10 +1237,10 @@ let discharge_autohint obj =
       | HintsVariables | HintsConstants -> grefs
       | HintsReferences grs ->
         let filter = function
-        | EvalConstRef c -> true
-        | EvalVarRef id -> not @@ Lib.is_in_section (GlobRef.VarRef id)
+        | EvalConstRef c -> Some (EvalConstRef (Lib.discharge_constant c))
+        | EvalVarRef id as x -> if not @@ Lib.is_in_section (GlobRef.VarRef id) then Some x else None
         in
-        let grs = List.filter filter grs in
+        let grs = List.filter_map filter grs in
         HintsReferences grs
       in
       AddTransparency { grefs; state }
@@ -1250,14 +1250,12 @@ let discharge_autohint obj =
     | AddCut path ->
       if is_section_path path then AddHints [] (* dummy *) else obj.hint_action
     | AddMode { gref; mode } ->
-      if Lib.is_in_section gref then
-        if isVarRef gref then AddHints [] (* dummy *)
-        else
-          let inst = Lib.section_instance gref in
+      (match Lib.discharge_global_reference_with_instance gref with
+       | None -> AddHints [] (* dummy *)
+       | Some (gref, inst) ->
           (* Default mode for discharged parameters is output *)
           let mode = Array.append (Array.make (Array.length inst) ModeOutput) mode in
-          AddMode { gref; mode }
-      else obj.hint_action
+          AddMode { gref; mode })
     in
     if is_trivial_action action then None
     else Some { obj with hint_action = action }
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 934a25031798..15741288a106 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -103,7 +103,7 @@ let classify_strategy (local,_) =
 
 let disch_ref ref =
   match ref with
-      EvalConstRef c -> Some ref
+      EvalConstRef c -> Some (EvalConstRef (Lib.discharge_constant c))
     | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref
 
 let discharge_strategy (local,obj) =
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 1c9c21d7d75e..1e1b3d978103 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -21,9 +21,10 @@ let cache_canonical_structure (o,_) =
   Instance.register ~warn:true env sigma o
 
 let discharge_canonical_structure (x, local) =
-  let gref = Instance.repr x in
-  if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
-  else Some (x, local)
+  if local then None else
+    match Instance.discharge x with
+    | Some x -> Some (x, local)
+    | None -> None
 
 let canon_cat = create_category "canonicals"
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 7d0b1484f23a..13b68d58df8c 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -126,8 +126,9 @@ let discharge_instance inst =
   match inst.locality with
   | Local -> None
   | SuperGlobal | Export ->
-    assert (not (isVarRef inst.instance));
-    Some inst
+    match Lib.discharge_global_reference inst.class_name, Lib.discharge_global_reference inst.instance with
+    | Some class_name, Some instance -> Some { inst with instance; class_name }
+    | _ -> None
 
 let classify_instance inst = match inst.locality with
 | Local -> Dispose
@@ -248,22 +249,27 @@ let subst_class (subst,cl) =
     cl_unique = cl.cl_unique }
 
 let discharge_class cl =
-  try
-    let info = Lib.section_segment_of_reference cl.cl_impl in
-    let info, _, cl_univs' = Cooking.lift_poly_univs info cl.cl_univs in
-    let nprops = List.length cl.cl_props in
-    let props, context = List.chop nprops (Discharge.cook_rel_context info (cl.cl_props @ cl.cl_context)) in
-    let discharge_proj x = x in
-    { cl_univs = cl_univs';
-      cl_impl = cl.cl_impl;
-      cl_context = context;
-      cl_props = props;
-      cl_projs = List.Smart.map discharge_proj cl.cl_projs;
-      cl_strict = cl.cl_strict;
-      cl_unique = cl.cl_unique
-    }
-  with Not_found -> (* not defined in the current section *)
-    cl
+  match Lib.discharge_global_reference cl.cl_impl with
+  | None -> None
+  | Some cl_impl ->
+    if Lib.is_in_section cl.cl_impl then
+      let info = Lib.section_segment_of_reference cl.cl_impl in
+      let info, _, cl_univs = Cooking.lift_poly_univs info cl.cl_univs in
+      let nprops = List.length cl.cl_props in
+      let cl_props, cl_context = List.chop nprops (Discharge.cook_rel_context info (cl.cl_props @ cl.cl_context)) in
+      let discharge_proj x =
+        { x with meth_const = Option.map Lib.discharge_constant x.meth_const } in
+      Some {
+        cl_univs;
+        cl_impl;
+        cl_context;
+        cl_props;
+        cl_projs = List.Smart.map discharge_proj cl.cl_projs;
+        cl_strict = cl.cl_strict;
+        cl_unique = cl.cl_unique;
+      }
+    else
+      Some cl
 
 let rebuild_class cl =
   try
@@ -277,7 +283,7 @@ let class_input : typeclass -> obj =
       cache_function = cache_class;
       load_function = (fun _ -> cache_class);
       classify_function = (fun x -> Substitute);
-      discharge_function = (fun a -> Some (discharge_class a));
+      discharge_function = discharge_class;
       rebuild_function = rebuild_class;
       subst_function = subst_class }
 
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 42fb37369b16..576a6b67bc1e 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -31,10 +31,10 @@ let subst_bidi_hints (subst, (gr, ohint as orig)) =
   if gr == gr' then orig else (gr', ohint)
 
 let discharge_bidi_hints (gr, ohint) =
-  if Globnames.isVarRef gr && Lib.is_in_section gr then None
-  else
-    let vars = Lib.section_instance gr in
-    let n = Array.length vars in
+  match Lib.discharge_global_reference_with_instance gr with
+  | None -> None
+  | Some (gr, inst) ->
+    let n = Array.length inst in
     Some (gr, Option.map ((+) n) ohint)
 
 let inBidiHints =
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 646859400525..73a2fda2acc8 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -238,13 +238,16 @@ let open_coercion i o =
 let discharge_coercion c =
   if c.coe_local then None
   else
-    let n =
-      try Array.length (Lib.section_instance c.coe_value)
-      with Not_found -> 0
-    in
+    match Lib.discharge_global_reference_with_instance c.coe_value with
+    | None -> None
+    | Some (v, inst) ->
+    let n = Array.length inst in
     let nc = { c with
       coe_param = n + c.coe_param;
       coe_is_projection = Option.map Lib.discharge_proj_repr c.coe_is_projection;
+      coe_value = v;
+      coe_source = discharge_coercion_class c.coe_source;
+      coe_target = discharge_coercion_class c.coe_target;
     } in
     Some nc
 
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 74fbb702c3ee..e346ea1aeaed 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -76,7 +76,7 @@ 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 discharge_prim (p,c) = Some (Lib.discharge_proj_repr p, Lib.discharge_constant c)
 
 let inPrim : (Projection.Repr.t * Constant.t) -> Libobject.obj =
   let open Libobject in
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 2acd27932a53..a7c9edfb4efd 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -84,7 +84,7 @@ let discharge_univ_names decl = match decl.udecl_src with
   | BoundUniv -> None
   | (QualifiedUniv _ | UnqualifiedUniv) -> Some decl
 
-let input_univ_names : universe_name_decl -> Libobject.obj =
+let inUnivNames : universe_name_decl -> Libobject.obj =
   let open Libobject in
   declare_named_object_gen
     { (default_object "Global universe name state") with
@@ -97,7 +97,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
 
 let input_univ_names (src, l, a) =
   if CList.is_empty l && CList.is_empty a then ()
-  else Lib.add_leaf (input_univ_names { udecl_src = src; udecl_named = l; udecl_anon = a })
+  else Lib.add_leaf (inUnivNames { udecl_src = src; udecl_named = l; udecl_anon = a })
 
 let label_of = let open GlobRef in function
 | ConstRef c -> Label.to_id @@ Constant.label c
diff --git a/vernac/record.ml b/vernac/record.ml
index ba22a83484b1..fc7115ac1aea 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -504,7 +504,7 @@ let cache_structure o = load_structure 1 o
 
 let subst_structure (subst, obj) = Structure.subst subst obj
 
-let discharge_structure x = Some x
+let discharge_structure x = Structure.discharge x
 
 let rebuild_structure s = Structure.rebuild (Global.env()) s