(* Nijmegen expects redefinition of sorts *)
Definition CProp := Prop.
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. *) 

Record 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}
}.