From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 test-suite/success/Record.v | 81 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 80 insertions(+), 1 deletion(-)

(limited to 'test-suite/success/Record.v')

diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 7fdbcda7..885fff48 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -1,3 +1,82 @@
 (* Nijmegen expects redefinition of sorts *)
 Definition CProp := Prop.
-Record test : CProp :=  {n : nat}.
+Record test : CProp :=  {n : nat ; m : bool ; _ : n <> 0 }.
+Require Import Program.
+Require Import List.
+
+Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
+Implicit Arguments vector [].
+
+Coercion vec_list : vector >-> list.
+
+Hint Rewrite @vec_len : datatypes.
+
+Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *).
+
+Obligation Tactic := crush.
+
+Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.
+
+Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := 
+  {| vec_list := cons a (vec_list v) |}.
+
+Hint Rewrite map_length rev_length : datatypes.
+
+Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := 
+  {| vec_list := map f v |}.
+
+Program Definition vreverse {A n} (v : vector A n) : vector A n := 
+  {| vec_list := rev v |}.
+
+Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := 
+  match v, w with
+    | nil, nil => nil
+    | cons f fs, cons x xs => cons (f x) (va_list fs xs)
+    | _, _ => nil
+  end.
+
+Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := 
+  {| vec_list := va_list v w |}.
+
+Next Obligation. 
+  destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
+  subst n. revert w Hw. induction v ; destruct w ; crush. 
+  rewrite IHv ; auto.
+Qed.
+
+(* Correct type inference of record notation. Initial example by Spiwack. *) 
+
+Inductive Machin := {
+ Bazar : option Machin
+}.
+
+Definition bli : Machin :=
+ {| Bazar := Some ({| Bazar := None |}:Machin) |}.
+
+Definition bli' : option (option Machin)  :=
+ Some (Some {| Bazar := None |} ).
+
+Definition bli'' : Machin :=
+ {| Bazar := Some {| Bazar := None |} |}.
+
+Definition bli''' := {| Bazar := Some {| Bazar := None |} |}.
+
+(** Correctly use scoping information *)
+
+Require Import ZArith.
+
+Record Foo := { bar : Z }.
+Definition foo := {| bar := 0 |}.
+
+(** Notations inside records *)
+
+Require Import Relation_Definitions.
+
+Record DecidableOrder : Type :=
+{ A : Type
+; le : relation A where "x <= y" := (le x y)
+; le_refl : reflexive _ le
+; le_antisym : antisymmetric _ le
+; le_trans : transitive _ le
+; le_total : forall x y, {x <= y}+{y <= x}
+}.
-- 
cgit v1.2.3