diff options
| author | Gaëtan Gilbert | 2018-02-20 00:27:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-09 16:29:06 +0100 |
| commit | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (patch) | |
| tree | 5b68a2bd48fc961987a193f4361c46f7b9940b33 /pretyping/reductionops.ml | |
| parent | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (diff) | |
Cumulativity: improve treatment of irrelevant universes.
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 0a28f1fb84..47e2ba93bd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1313,10 +1313,10 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_check_inductive_instances csts sigma = - try Evd.add_constraints sigma csts - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> +let sigma_check_inductive_instances cv_pb variance u1 u2 sigma = + match Evarutil.compare_cumulative_instances cv_pb variance u1 u2 sigma with + | Inl sigma -> sigma + | Inr _ -> raise Reduction.NotConvertible let sigma_univ_state = |