diff --git a/interp/impargs.ml b/interp/impargs.ml
index 83804729397d..2ccb804a4dd4 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -602,19 +602,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
@@ -623,8 +628,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 f361227fb491..caae05d72aa8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1983,13 +1983,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/names.ml b/kernel/names.ml
index 9498b0587ccf..003032afe314 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -386,6 +386,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
 
@@ -508,6 +514,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)
 
@@ -619,6 +629,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
@@ -667,6 +679,8 @@ struct
 
   let modpath (ind, _) = Ind.modpath ind
 
+  let pop (ind,i) = (Ind.pop ind, i)
+
   module CanOrd =
   struct
     type nonrec t = t
@@ -821,6 +835,8 @@ struct
 
     let arg c = c.proj_arg
 
+    let pop p = { p with proj_ind = Ind.pop p.proj_ind }
+
     let hash p =
       Hashset.Combine.combinesmall p.proj_arg (Ind.CanOrd.hash p.proj_ind)
 
@@ -920,6 +936,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 77176b8450a3..a37369e66705 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
@@ -589,6 +604,7 @@ module Projection : sig
     val npars : t -> int
     val arg : t -> int
     val label : t -> Label.t
+    val pop : t -> t
 
     val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"]
     val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"]
@@ -619,6 +635,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/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/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 21c9357737a1..880bf634f8fc 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 UVars.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 7a1b4a9c8d81..dc8034048cc4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -287,6 +287,22 @@ 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 = mind
+
+let discharge_inductive ind = ind
+
+let discharge_constant cst = cst
+
+let discharge_constant_with_instance cst = (discharge_constant cst, section_instance (GlobRef.ConstRef cst))
+
+let discharge_global_reference ref = Some ref
+
+let discharge_global_reference_with_instance ref =
+  if is_in_section ref then
+    if Globnames.isVarRef ref then None
+    else Some (ref, section_instance ref)
+  else Some (ref, [||])
+
 let discharge_item = Libobject.(function
   | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
   | ExportObject _ -> None
diff --git a/library/lib.mli b/library/lib.mli
index 29cbbe0f26f7..4a3f6c2a8bc3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -173,6 +173,13 @@ 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_constant_with_instance : Constant.t -> Constant.t * Constr.t array
+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 106ae896bdf0..1db10f375775 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 3693abfe137e..bca9860708f8 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 479bb84ceb8b..5ce8da5fb88c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -106,18 +106,12 @@ module ReductionBehaviour = struct
     let r' = subst_constant subst r in if r==r' then orig
     else (local,(r',o))
 
-  let discharge = function
-    | false, (gr, b) ->
-      let b =
-        let gr = GlobRef.ConstRef gr in
-        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
-      Some (false, (gr, b))
-    | true, _ -> None
+  let discharge (local, (cst, b)) =
+    if local then None
+    else
+      let (cst, inst) = Lib.discharge_constant_with_instance cst in
+      let b = more_args (Array.length inst) b in
+      Some (false, (cst, b))
 
   let inRedBehaviour = declare_object {
       (default_object "REDUCTIONBEHAVIOUR") with
diff --git a/pretyping/structures.ml b/pretyping/structures.ml
index 203b9f1c0f35..1ca3f00d37cd 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 96c34697f17e..a51e7bc9b4cd 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 f639016fec01..f556729b9591 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1289,10 +1289,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 }
@@ -1302,14 +1302,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 64bfee344ed1..e42a4cce562a 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -101,7 +101,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 536cc5953c1c..449e0fa00d5a 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 00206c9c5451..2a423694e39d 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 3f633c00b22f..1792ab69f4b1 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/record.ml b/vernac/record.ml
index 938a726d94ec..34404a56a310 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -505,7 +505,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