diff options
| author | Théo Zimmermann | 2018-07-02 19:04:42 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-02 19:04:42 +0200 |
| commit | b7d81ff8e1c715a3fe587d6bcaa6d132647ebd30 (patch) | |
| tree | f1eedbdcc3aa8af12b9f39be2c02f16590fe1a1c /doc/sphinx/language | |
| parent | 0a556686f5c759e61dc740dd1b2762a077a19f40 (diff) | |
| parent | 2ecec19501ebc3c98033fe1f212e85731473e2c7 (diff) | |
Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index c26ae2a93b..ec99ccbeea 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -38,6 +38,7 @@ At the end, the notation “``[entry sep … sep entry]``” stands for a possibly empty sequence of expressions parsed by the “``entry``” entry, separated by the literal “``sep``”. +.. _lexical-conventions: Lexical conventions =================== |