From 88286ec054a82b91b56c69091d7daca585cea1b2 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 14 May 2020 12:56:39 +0200
Subject: Fix title level and a build failure.

---
 doc/sphinx/language/extensions/evars.rst | 2 +-
 doc/sphinx/language/extensions/match.rst | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

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`
 -------------------------------------
-- 
cgit v1.2.3