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. --- test-suite/success/polymorphism.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9167c9fcb..dc22b03f2 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