diff options
Diffstat (limited to 'doc/sphinx/language/gallina-specification-language.rst')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 46e684b12..39735a6ed 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -609,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``. Adds blocks of variables with different specifications. .. cmdv:: Variables {+ ( {+ @ident } : @term) } + :name: Variables .. cmdv:: Hypothesis {+ ( {+ @ident } : @term) } :name: Hypothesis @@ -672,6 +673,7 @@ Section :ref:`typing-rules`. You have to explicitly give their fully qualified name to refer to them. .. cmdv:: Example @ident := @term + :name: Example .. cmdv:: Example @ident : @term := @term |