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 +++-
 test-suite/success/polymorphism.v | 16 ++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

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;
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9167c9fcbf..dc22b03f2d 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -292,3 +292,19 @@ Section foo2.
   Context `{forall A B, Funext A B}.
   Print Universes.
 End foo2.
+
+Module eta.
+Set Universe Polymorphism.
+
+Set Printing Universes.
+
+Axiom admit : forall A, A.
+Record R := {O : Type}.
+
+Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
+Definition RLRL' : forall x : R, RL x = RL (RL x).
+  intros. apply eq_refl.
+Qed.
+
+End eta.
-- 
cgit v1.2.3