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