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.
---
 pretyping/reductionops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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