From 437b91a3ffd7327975a129b95b24d3f66ad7f3e4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 30 Aug 2014 18:48:11 +0200
Subject: Simplify even further the declaration of primitive projections, now
 done entirely using declare_mind, which declares the associated constants for
 primitive records. This avoids a hack related to elimination schemes and
 ensures that the forward references to constants in the mutual inductive
 entry are properly declared just after the inductive. This also clarifies
 (and simplifies) the code of term_typing for constants which does not have to
 deal with building or checking projections anymore. Also fix printing of
 universes showing the de Bruijn encoding in a few places.

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

(limited to 'test-suite')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
new file mode 100644
index 0000000000..2682df3b72
--- /dev/null
+++ b/test-suite/success/primitiveproj.v
@@ -0,0 +1,30 @@
+Set Primitive Projections.
+Set Record Elimination Schemes.
+Module Prim.
+
+Record F := { a : nat; b : a = a }.
+Record G (A : Type) := { c : A; d : F }.
+
+Check c.
+End Prim.
+Module Univ.
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Record Foo (A : Type) := { foo : A }.
+
+Record G (A : Type) := { c : A; d : c = c; e : Foo A }.
+
+Definition Foon : Foo nat := {| foo := 0 |}.
+
+Definition Foonp : nat := Foon.(foo).
+
+Definition Gt : G nat := {| c:= 0; d:=eq_refl; e:= Foon |}.
+
+Check (Gt.(e)).
+
+Section bla.
+
+  Record bar := { baz : nat; def := 0; baz' : forall x, x = baz \/ x = def }.
+End bla.
+
+End Univ.
-- 
cgit v1.2.3