diff options
| author | Maxime Dénès | 2018-04-16 21:26:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-16 23:29:00 +0200 |
| commit | a3ee82e80083fff971e382f52d9295fda2210e2d (patch) | |
| tree | c33240b821d78fb63bd0a3bb0a8d2bf17507f6c2 /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | abd6bbd90753fd98355e551d8dc8ecfd07494639 (diff) | |
[Sphinx] Clean-up indices
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9965d5002d..c4a7121ce4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -32,6 +32,8 @@ Notations Basic notations ~~~~~~~~~~~~~~~ +.. cmd:: Notation + A *notation* is a symbolic expression denoting some term or term pattern. @@ -1200,7 +1202,7 @@ Tactic notations allow to customize the syntax of the tactics of the tactic language. Tactic notations obey the following syntax: .. productionlist:: coq - tacn : [Local] Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. + tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `natural`) tactic_argument_type : ident | simple_intropattern | reference @@ -1211,7 +1213,7 @@ tactic language. Tactic notations obey the following syntax: : | tactic | tactic0 | tactic1 | tactic2 | tactic3 : | tactic4 | tactic5 -.. cmd:: {? Local} Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. +.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the |