Abstract discharge functions over how names are themselves discharged

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 ->

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 *)

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'
 

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"]

library/coqlib.ml

@@ -64,14 +64,19 @@ 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
     cache_function = cache_ref;
     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 =

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

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

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

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

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

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
 

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

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
 

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

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