From 02663c526a3fd347fad803eb664d22e6b5c088ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 28 Jun 2015 15:23:00 +0200
Subject: Fix incompleteness of conversion used by evarconv

In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
---
 pretyping/reductionops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dd671f111e..dc70f36ccf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1287,7 +1287,9 @@ let sigma_compare_sorts env pb s0 s1 sigma =
     
 let sigma_compare_instances flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
-  with Evd.UniversesDiffer -> raise Reduction.NotConvertible
+  with Evd.UniversesDiffer
+     | Univ.UniverseInconsistency _ ->
+	raise Reduction.NotConvertible
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
-- 
cgit v1.2.3