From c907f31fd8f4b12bf2d7df2078603dbe804475a2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 4 Sep 2014 00:40:12 +0200
Subject: Add test-suite file for Case derivation on primitive records.

---
 test-suite/success/letproj.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/success/letproj.v

(limited to 'test-suite')

diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v
new file mode 100644
index 0000000000..a183be6223
--- /dev/null
+++ b/test-suite/success/letproj.v
@@ -0,0 +1,9 @@
+Set Primitive Projections.
+Set Record Elimination Schemes.
+Record Foo (A : Type) := { bar : A -> A; baz : A }.
+
+Definition test (A : Type) (f : Foo A) := 
+  let (x, y) := f in x.
+
+Scheme foo_case := Case for Foo Sort Type.
+
-- 
cgit v1.2.3