From c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 10:42:41 +0100 Subject: Using a dedicated type for Lib.abstr_info. --- pretyping/arguments_renaming.ml | 8 +------- pretyping/reductionops.ml | 6 +++--- pretyping/typeclasses.ml | 3 ++- 3 files changed, 6 insertions(+), 11 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3 From bad3f3b784d3de8851615b8f4b7afba734232d8e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 17:33:04 +0100 Subject: Moving some universe substitution code out of the kernel. This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper. --- pretyping/unification.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b41fb4e4dd..8df8f84742 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module CVars = Vars - open CErrors open Pp open Util @@ -1527,7 +1525,7 @@ let indirectly_dependent sigma c d decls = let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1617,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | Some (sigma,_,l) -> let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) let make_eq_test env evd c = let out cstr = -- cgit v1.2.3