diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 11 | ||||
| -rw-r--r-- | pretyping/univdecls.ml | 2 |
2 files changed, 10 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0a63985bf1..fe2e86a482 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -530,8 +530,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd, NotSameHead) else begin - let evd' = check_leq_inductives evd cumi u u' in - Success (check_leq_inductives evd' cumi u' u) + (** Both constructors should be liftable to the same supertype + at which we compare them, but we don't have access to that type in + untyped unification. We hence try to enforce that one is lower + than the other, also unifying more universes in the process. + If this fails we just leave the universes as is, as in conversion. *) + try Success (check_leq_inductives evd cumi u u') + with Univ.UniverseInconsistency _ -> + try Success (check_leq_inductives evd cumi u' u) + with Univ.UniverseInconsistency e -> Success evd end end in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index d16f046fab..8864be5761 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -38,7 +38,7 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open Misctypes in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; |