Record.v « success « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/success/Record.v

blob: 7fdbcda7bcb4035c5dc3abfd6cb1829fa23511c6 (plain)

1
2
3

(* Nijmegen expects redefinition of sorts *)
Definition CProp := Prop.
Record test : CProp :=  {n : nat}.