diff options
| author | Théo Zimmermann | 2020-05-14 12:56:39 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 15:10:10 +0200 |
| commit | 88286ec054a82b91b56c69091d7daca585cea1b2 (patch) | |
| tree | 93481007ff282c07f150dfb5f57e568dd46a6b36 | |
| parent | efa36e61d6eb5421c3c16d66c6d390268892edf2 (diff) | |
Fix title level and a build failure.
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 7635441c24..40e0898871 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -69,7 +69,7 @@ with a named-goal selector, see :ref:`goal-selectors`). .. index:: _ Inferable subterms ------------------- +~~~~~~~~~~~~~~~~~~ Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index b83e11e253..028d0aaf57 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -9,7 +9,7 @@ This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides - .. extracted from Gallina extensions chapter +.. extracted from Gallina extensions chapter Variants and extensions of :g:`match` ------------------------------------- |