aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools/coqrst/notations/TacticNotations.g
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
-rw-r--r--doc/tools/coqrst/notations/TacticNotations.g30
1 files changed, 30 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
new file mode 100644
index 000000000..72ae8eb6b
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -0,0 +1,30 @@
+/************************************************************************/
+/* * The Coq Proof Assistant / The Coq Development Team */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* <O___,, * (see CREDITS file for the list of authors) */
+/* \VV/ **************************************************************/
+/* // * This file is distributed under the terms of the */
+/* * GNU Lesser General Public License Version 2.1 */
+/* * (see LICENSE file for the text of the license) */
+/************************************************************************/
+grammar TacticNotations;
+
+// Terminals are not visited, so we add non-terminals for each terminal that
+// needs rendering (in particular whitespace (kept in output) vs. WHITESPACE
+// (discarded)).
+
+top: blocks EOF;
+blocks: block ((whitespace)? block)*;
+block: atomic | hole | repeat | curlies;
+repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
+curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
+whitespace: WHITESPACE;
+atomic: ATOM;
+hole: ID;
+
+LGROUP: '{' [+*?];
+LBRACE: '{';
+RBRACE: '}';
+ATOM: ~[@{} ]+;
+ID: '@' [a-zA-Z0-9_]+;
+WHITESPACE: ' '+;