diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-02 19:04:42 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 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 c26ae2a93..ec99ccbee 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 =================== |