From 501d6dd5691474c807a722d9b5b6e3fa9d83c749 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 18:51:48 +0200
Subject: Tactical `progress` compares term up to potentially equalisable
 universes.

Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.

As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.---
 test-suite/bugs/closed/3593.v | 10 ++++++++++
 test-suite/bugs/opened/3593.v | 10 ----------
 2 files changed, 10 insertions(+), 10 deletions(-)
 create mode 100644 test-suite/bugs/closed/3593.v
 delete mode 100644 test-suite/bugs/opened/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..378db68570
--- /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.
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v
deleted file mode 100644
index d83b900607..0000000000
--- a/test-suite/bugs/opened/3593.v
+++ /dev/null
@@ -1,10 +0,0 @@
-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 Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
-  reflexivity.
-Qed.
-- 
cgit v1.2.3