From d06211803146dec998b414d215d4d93190e2001f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 28 Nov 2016 18:36:10 +0100
Subject: 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.
---
 kernel/reduction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/reduction.ml')

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) =
-- 
cgit v1.2.3