aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3625.v
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-29 00:10:43 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-29 00:19:04 +0200
commit6e22ae3f21ae32f298b6e3463448f59a5c7d1f76 (patch)
tree1408ca239b7153725c7a77195c6ab3f39ec27d7d /test-suite/bugs/closed/3625.v
parent199bb343f7e4367d843ab5ae76ba9a4de89eddbc (diff)
In evarconv and unification, expand folded primitive projections to
their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly.
Diffstat (limited to 'test-suite/bugs/closed/3625.v')
-rw-r--r--test-suite/bugs/closed/3625.v9
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3625.v b/test-suite/bugs/closed/3625.v
new file mode 100644
index 000000000..a0f977eea
--- /dev/null
+++ b/test-suite/bugs/closed/3625.v
@@ -0,0 +1,9 @@
+Set Implicit Arguments.
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+
+Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _).
+ intros.
+ apply f_equal.
+ admit.
+Qed.