From 98b79e9bf4ac082f948e381a68b8219fc3f3c314 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Apr 2018 11:59:48 +0200
Subject: [sphinx] Backport reformulation.

(cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
---
 doc/sphinx/proof-engine/tactics.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6c1b1c08c1..76796c934f 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2430,8 +2430,8 @@ subgoals.
         In particular a failure will happen if any of these three simpler tactics
         fails.
       + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses
-        :g:`H`:sub:`i` :g:`<> H`. A success will happen as soon as at least one of these
-        simpler tactics succeeds.
+        :g:`H`:sub:`i` different from :g:`H`.
+        A success will happen as soon as at least one of these simpler tactics succeeds.
       + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-`
         that succeeds if at least one of these two tactics succeeds.
 
-- 
cgit v1.2.3