diff options
| -rw-r--r-- | kernel/declarations.mli | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 4 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 15 | ||||
| -rw-r--r-- | kernel/inductive.ml | 9 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
9 files changed, 21 insertions, 21 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index b8dfe63d3..85dac4bfc 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -27,7 +27,7 @@ type engagement = ImpredicativeSet *) type template_arity = { - template_param_levels : Univ.universe option list; + template_param_levels : Univ.universe_level option list; template_level : Univ.universe; } diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 55868097f..dd906bab2 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -31,8 +31,8 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = - { template_param_levels = - List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels; + { template_param_levels = ar.template_param_levels; + (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0f9c7421f..85d04e5e2 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -195,11 +195,11 @@ let is_impredicative env u = let param_ccls params = let has_some_univ u = function - | Some v when Universe.equal u v -> true + | Some v when Univ.Level.equal u v -> true | _ -> false in let remove_some_univ u = function - | Some v when Universe.equal u v -> None + | Some v when Univ.Level.equal u v -> None | x -> x in let fold l (_, b, p) = match b with @@ -210,10 +210,13 @@ let param_ccls params = (* polymorphism unless there is aliasing (i.e. non distinct levels) *) begin match kind_of_term c with | Sort (Type u) -> - if List.exists (has_some_univ u) l then - None :: List.map (remove_some_univ u) l - else - Some u :: l + (match Univ.Universe.level u with + | Some u -> + if List.exists (has_some_univ u) l then + None :: List.map (remove_some_univ u) l + else + Some u :: l + | None -> None :: l) | _ -> None :: l end diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8d6f757b6..3f1c4e75f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -155,10 +155,7 @@ let sort_as_univ = function (* Template polymorphism *) let cons_subst u su subst = - try - (u, sup su (List.assoc_f Universe.equal u subst)) :: - List.remove_assoc_f Universe.equal u subst - with Not_found -> (u, su) :: subst + Univ.LMap.add u su subst let actualize_decl_level env lev t = let sign,s = dest_arity env t in @@ -192,7 +189,7 @@ let rec make_subst env = function d::ctx, subst | sign, [], _ -> (* Uniform parameters are exhausted *) - sign,[] + sign, Univ.LMap.empty | [], _, _ -> assert false @@ -201,7 +198,7 @@ exception SingletonInductiveBecomesProp of Id.t let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in - let level = subst_large_constraints subst ar.template_level in + let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) if is_type0m_univ level then prop_sort diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c6355b3ea..49f883628 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign = let extract_level env p = let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Some u | _ -> None + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = let fold l (_, b, p) = match b with diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0ddc7c006..cce6aff28 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -207,7 +207,7 @@ let oib_equal o1 o2 = | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> eq_constr c1 c2 && Sorts.equal s1 s2 | TemplateArity p1, TemplateArity p2 -> - let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in + let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in List.equal eq p1.template_param_levels p2.template_param_levels && Univ.Universe.equal p1.template_level p2.template_level | _, _ -> false diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d6b18175b..18c91c0e3 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -830,7 +830,7 @@ let get_template_constructor_type evdref (ind, i) n = | Some u :: l, Prod (na, t, t') -> let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in (* evdref := set_leq_sort !evdref u'l (Type u); *) - let s = Univ.LMap.add (Option.get (Univ.Universe.level u)) + let s = Univ.LMap.add u (Option.get (Univ.Universe.level u')) Univ.LMap.empty in let dom = subst_univs_level_constr s t in (* let codom = subst_univs_level_constr s t' in *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7715691b0..aa302bac6 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -221,7 +221,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> (* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *) val get_template_constructor_type : evar_map ref -> constructor -> int -> - (Univ.universe option list * types) + (Univ.universe_level option list * types) val get_template_inductive_type : evar_map ref -> inductive -> int -> - (Univ.universe option list * types) + (Univ.universe_level option list * types) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0b7cd89f2..e180c1346 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -465,7 +465,7 @@ let rec instantiate_universes env evdref scl is = function let s = (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) - if univ_depends u is then + if univ_depends (Univ.Universe.make u) is then scl (* constrained sort: replace by scl *) else (* unconstriained sort: replace by fresh universe *) |