diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d6b18175b4..18c91c0e30 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 7715691b0c..aa302bac6f 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 0b7cd89f25..e180c13465 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 *) |