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 /kernel/reduction.ml | |
| 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 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6c664f7918..1ae89347ad 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let cuniv = conv_table_key infos fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with NotConvertible -> + with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = |