diff options
| author | Théo Zimmermann | 2018-11-28 16:03:11 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-11-30 00:31:13 +0100 |
| commit | f1fa3386a01f06884fe7f71796a558eae3bb3e00 (patch) | |
| tree | b6afbc5f8ea20cb95df9437a536b524c6324947e /doc/sphinx/language | |
| parent | 4b12cd00e1d32961a4dc04e2c2dcbfe6ed0002fa (diff) | |
Add indexes for coercion / substructure symbol :>.
And a few more Sphinx fixes in passing.
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..10650af1d1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,8 +97,8 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! |