diff options
| author | Pierre-Marie Pédrot | 2017-12-13 10:42:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-12-30 19:19:03 +0100 |
| commit | c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c (patch) | |
| tree | 995ef76564fb951d0dd84a5834d05bbe27b5d239 /pretyping | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Using a dedicated type for Lib.abstr_info.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 8 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 3 |
3 files changed, 6 insertions, 11 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index d59102b6c7..8ac471404a 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -40,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) = let r' = fst (subst_global subst r) in if r==r' then orig else (r', names) -let section_segment_of_reference = function - | ConstRef con -> Lib.section_segment_of_constant con - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.AUContext.empty - let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> (try - let vars,_,_ = section_segment_of_reference c in + let vars = Lib.variable_section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in let names' = var_names @ names in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ac88468545..78de0437d0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -121,10 +121,10 @@ module ReductionBehaviour = struct let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) let discharge = function - | _,(ReqGlobal (ConstRef c, req), (_, b)) -> + | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) -> let b = - if Lib.is_in_section (ConstRef c) then - let vars, _, _ = Lib.section_segment_of_constant c in + if Lib.is_in_section gr then + let vars = Lib.variable_section_segment_of_reference gr in let extra = List.length vars in let nargs' = if b.b_nargs = max_int then max_int diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index f153b63410..3f947fd23f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -219,7 +219,8 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, _, _ as info = abs_context cl in + let info = abs_context cl in + let ctx = info.Lib.abstr_ctx in let ctx, subst = rel_of_variable_context ctx in let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in |