Record.v « success « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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