plik.v « modules « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/modules/plik.v

blob: f1f59df0f4cd43b78a35ef336a88b002d4184782 (plain)

Definition toto:=[x:Set]x.

Grammar constr constr8 := 
     toto [ "#" constr7($b) ] -> [ (toto $b) ].