Fix title level and a build failure.

coq · May 14, 2020 · 88286ec · 88286ec
1 parent efa36e6
commit 88286ec
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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`
 -------------------------------------