add test for unfolding primitive projections

3 files changed, 62 insertions, 0 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
index ef657d5..2aaaf9e 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -158,6 +158,7 @@ ssrtest/move_after.v
 ssrtest/multiview.v
 ssrtest/occarrow.v
 ssrtest/patnoX.v
+ssrtest/primproj.v
 ssrtest/rewpatterns.v
 ssrtest/set_lamda.v
 ssrtest/set_pattern.v
diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make
index ab4c666..6033c13 100644
--- a/mathcomp/ssrtest/Make
+++ b/mathcomp/ssrtest/Make
@@ -26,6 +26,7 @@ move_after.v
 multiview.v
 occarrow.v
 patnoX.v
+primproj.v
 rewpatterns.v
 set_lamda.v
 set_pattern.v
diff --git a/mathcomp/ssrtest/primproj.v b/mathcomp/ssrtest/primproj.v
new file mode 100644
index 0000000..25afb28
--- /dev/null
+++ b/mathcomp/ssrtest/primproj.v
@@ -0,0 +1,60 @@
+From mathcomp Require Import ssreflect.
+
+
+Set Primitive Projections.
+
+Module T1.
+
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Goal foo_car _ bar = 10.
+match goal with
+| |- foo_car _ bar = 10 => idtac
+end.
+rewrite /foo_car.
+Fail match goal with
+| |- foo_car _ bar = 10 => idtac
+end.
+Admitted.
+
+End T1.
+
+
+Module T2.
+
+Record foo {A} := Foo { foo_car : A }.
+
+Definition bar : foo := Foo nat 10.
+
+Goal foo_car bar = 10.
+match goal with
+| |- foo_car bar = 10 => idtac
+end.
+rewrite /foo_car.
+Fail match goal with
+| |- foo_car bar = 10 => idtac
+end.
+Admitted.
+
+End T2.
+
+
+Module T3.
+
+Record foo {A} := Foo { foo_car : A }.
+
+Definition bar : foo := Foo nat 10.
+
+Goal foo_car bar = 10.
+rewrite -[foo_car _]/(id _).
+match goal with |- id _ = 10 => idtac end.
+Admitted.
+
+Goal foo_car bar = 10.
+set x := foo_car _.
+match goal with |- x = 10 => idtac end.
+Admitted.
+
+End T3.
\ No newline at end of file