aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/coq/parsingcheck-410.v
diff options
context:
space:
mode:
Diffstat (limited to 'etc/coq/parsingcheck-410.v')
-rw-r--r--etc/coq/parsingcheck-410.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/etc/coq/parsingcheck-410.v b/etc/coq/parsingcheck-410.v
index 29e84e58..37a7e57f 100644
--- a/etc/coq/parsingcheck-410.v
+++ b/etc/coq/parsingcheck-410.v
@@ -1 +1,3 @@
-Require Export Coq.Lists.List. Notation "[ ]" := nil : list_scope. Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+Require Export Coq.Lists.List.
+Notation "[ ]" := nil : list_scope.
+Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.