parsingcheck-410.v « coq « etc - proof-general - Emacs interface for proof assistants

about summary refs log tree commit diff homepage

path: root/etc/coq/parsingcheck-410.v

blob: 29e84e58859bc4f6edbe74929ff2de9ca29db893 (plain)

1	`Require Export Coq.Lists.List. Notation "[ ]" := nil : list_scope. Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.`