From f96dc97f48df5d0fdf252be5f28478a58be77961 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Sep 2014 20:51:40 +0200
Subject: Fix bug #3593, making constr_eq and progress work up to equality of
 universes, along with a few other functions in evd.

---
 test-suite/bugs/closed/3593.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/3593.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v
new file mode 100644
index 0000000000..25f9db6b28
--- /dev/null
+++ b/test-suite/bugs/closed/3593.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+Set Printing All.
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
+simpl; intros.
+  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
+  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). 
+  reflexivity.
+Qed.
-- 
cgit v1.2.3