diff options
| author | Matthieu Sozeau | 2016-11-28 18:36:10 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-30 15:43:12 +0100 |
| commit | d06211803146dec998b414d215d4d93190e2001f (patch) | |
| tree | 6847ddc614130284e0e83e465496cfbbd63daed3 /pretyping | |
| parent | a27ac0315dcbb99c64a260bac3988199a26b39cf (diff) | |
Univs: fix bug #5180
In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 332d4e0b26..297f0a1a8e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1262,7 +1262,7 @@ let sigma_compare_sorts env pb s0 s1 sigma = match pb with | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1 | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 - + let sigma_compare_instances ~flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 with Evd.UniversesDiffer |