From de7f7fe34828debfa4bd5130810ee5ccc0ea0170 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 28 Jan 2021 13:20:07 -0800
Subject: Update doc/sphinx/proofs/writing-proofs/rewriting.rst

---
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 3d902a9c76..f286533d78 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -109,7 +109,7 @@ Rewriting with Leibniz and setoid equality
 
       For each selected hypothesis and/or the conclusion,
       :tacn:`rewrite` finds the first matching subterm in
-      depth-first search order. Only subterms identical to the
+      depth-first search order. Only subterms identical to
       that first matched subterm are rewritten.  If the `at` clause is specified,
       only these subterms are considered when counting occurrences.
       To select a different set of matching subterms, you can
-- 
cgit v1.2.3