From b3c82cbe2b7feafb254af316b5c4a8032e8cf8b3 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 23 Jul 2019 00:35:24 +0200
Subject: doc: Fix a detail in 2 files describing the under tactic

href: coq/coq#9651
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 1b9e3ce0f3..ed980bd4de 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3761,10 +3761,10 @@ involves the following steps:
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
-   These protected goals are displayed using the ``Under[ … ]``
-   notation (e.g. ``Under[ m - m ]`` in the running example).
+   These protected goals are displayed using the ``'Under[ … ]``
+   notation (e.g. ``'Under[ m - m ]`` in the running example).
 
-6. The expression inside the ``Under[ … ]`` notation can be
+6. The expression inside the ``'Under[ … ]`` notation can be
    proved equivalent to the desired expression
    by using a regular :tacn:`rewrite` tactic.
 
@@ -3782,7 +3782,7 @@ The over tactic
 
 Two equivalent facilities (a terminator and a lemma) are provided to
 close intermediate subgoals generated by :tacn:`under` (i.e. goals
-displayed as ``Under[ … ]``):
+displayed as ``'Under[ … ]``):
 
 .. tacn:: over
    :name: over
@@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``):
 
 .. tacv:: by rewrite over
 
-   This is a variant of :tacn:`over` in order to close ``Under[ … ]``
+   This is a variant of :tacn:`over` in order to close ``'Under[ … ]``
    goals, relying on the ``over`` rewrite rule.
 
 .. _under_one_liner:
-- 
cgit v1.2.3