diff options
| author | Clément Pit-Claudel | 2018-11-30 10:57:39 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-11-30 10:57:39 -0500 |
| commit | 6cafa55b58054da0b7366bea4e10a06147640eee (patch) | |
| tree | b94e3086e6681c05720f7d50e2dda545a50f7aee /doc/sphinx/language | |
| parent | ea5207f2b13862408fd67cfac8d3a079ed80a087 (diff) | |
| parent | f1fa3386a01f06884fe7f71796a558eae3bb3e00 (diff) | |
Merge PR #9105: Add indexes for coercion / substructure symbol :>.
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! |