aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/language
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-02 19:04:42 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-02 19:04:42 +0200
commitb7d81ff8e1c715a3fe587d6bcaa6d132647ebd30 (patch)
treef1eedbdcc3aa8af12b9f39be2c02f16590fe1a1c /doc/sphinx/language
parent0a556686f5c759e61dc740dd1b2762a077a19f40 (diff)
parent2ecec19501ebc3c98033fe1f212e85731473e2c7 (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.rst1
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
===================