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: f3a13634df97fadcbc7c50b863435be48cf064c8 (plain)

1
2
3

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