diff options
| author | Théo Zimmermann | 2018-04-13 11:05:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-14 15:44:29 +0200 |
| commit | 3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (patch) | |
| tree | 6846570d84758373da6bffa36b3bb8e285703aa4 /doc/sphinx/language/gallina-specification-language.rst | |
| parent | 14f44c0e23c413314adf23ed1059acc5cd1fef2f (diff) | |
[sphinx] Fix many warnings.
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
Diffstat (limited to 'doc/sphinx/language/gallina-specification-language.rst')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 2a146c57aa..6458ceeaaf 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -13,7 +13,7 @@ language of commands, called *The Vernacular* is described in Section :ref:`vernacular`. In Coq, logical objects are typed to ensure their logical correctness. The -rules implemented by the typing algorithm are described in Chapter :ref:`cic`. +rules implemented by the typing algorithm are described in Chapter :ref:`calculusofinductiveconstructions`. About the grammars in the manual @@ -110,6 +110,8 @@ Special tokens longest possible one (among all tokens defined at this moment), and so on. +.. _term: + Terms ===== @@ -118,9 +120,9 @@ Syntax of terms The following grammars describe the basic syntax of the terms of the *Calculus of Inductive Constructions* (also called Cic). The formal -presentation of Cic is given in Chapter :ref:`cic`. Extensions of this syntax -are given in Chapter :ref:`gallinaextensions`. How to customize the syntax -is described in Chapter :ref:`syntaxextensions`. +presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`. Extensions of this syntax +are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax +is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. .. productionlist:: coq term : forall `binders` , `term` @@ -201,9 +203,9 @@ Numerals Numerals have no definite semantics in the calculus. They are mere notations that can be bound to objects through the notation mechanism -(see Chapter :ref:`syntaxextensions` for details). +(see Chapter :ref:`syntaxextensionsandinterpretationscopes` for details). Initially, numerals are bound to Peano’s representation of natural -numbers (see :ref:`libnats`). +numbers (see :ref:`datatypes`). .. note:: @@ -484,6 +486,8 @@ The association of a single fixpoint and a local definition have a special syntax: “let fix f … := … in …” stands for “let f := fix f … := … in …”. The same applies for co-fixpoints. +.. _vernacular: + The Vernacular ============== @@ -605,6 +609,8 @@ logical postulates (i.e. when the assertion *term* is of sort ``Prop``), and to use the keywords ``Parameter`` and ``Variable`` in other cases (corresponding to the declaration of an abstract mathematical entity). +.. _gallina_def: + Definitions ----------- |