From 69c8917e3bdc8678baf1358ead549acff2f52ca2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 22 Aug 2018 15:53:09 +0200
Subject: Fix #8251: remove "the the" occurrences

---
 doc/tools/coqrst/coqdomain.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index e6b71a8293..a0dc16aac7 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -449,7 +449,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
        it names the introduced hypothesis :token:`ident`.
 
     Note that this example also uses ``:token:``.  That's because ``ident`` is
-    defined in the the Coq manual as a grammar production, and ``:token:``
+    defined in the Coq manual as a grammar production, and ``:token:``
     creates a link to that.  When referring to a placeholder that happens to be
     a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
     """
-- 
cgit v1.2.3