diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-28 15:23:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-28 15:27:38 +0200 |
| commit | 02663c526a3fd347fad803eb664d22e6b5c088ad (patch) | |
| tree | 32ac40ac32acbd4a5363fa1fb912672a66c090f4 /test-suite/success/polymorphism.v | |
| parent | 902ce91fd6006e6df57a8d5133676981967d49b4 (diff) | |
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.
Diffstat (limited to 'test-suite/success/polymorphism.v')
| -rw-r--r-- | test-suite/success/polymorphism.v | 16 |
1 files changed, 16 insertions, 0 deletions
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. |