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/changes.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/changes.rst')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index fd84868a1f..6ac55e7bf4 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes:
     extensionality lemma:
 
     - interactive mode: :n:`under @term`, associated terminator: :tacn:`over`
-    - one-liner mode: `under @term do [@tactic | ...]`
+    - one-liner mode: :n:`under @term do [@tactic | ...]`
 
     It can take occurrence switches, contextual patterns, and intro patterns:
-    :g:`under {2}[in RHS]eq_big => [i|i ?] do ...`
+    :g:`under {2}[in RHS]eq_big => [i|i ?]`
     (`#9651 <https://github.com/coq/coq/pull/9651>`_,
     by Erik Martin-Dorel and Enrico Tassi).
 
-- 
cgit v1.2.3