diff options
| -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` ------------------------------------- |