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

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b379cdf410..ec0ff73062 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -633,7 +633,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
           dependency status (of course, Anonymous implies non
           dependent, but not conversely).
 
-          From Coq > 8.2, using or not the the effective dependency of
+          From Coq > 8.2, using or not the effective dependency of
           the predicate is parametrable! *)
 
           begin match na with
-- 
cgit v1.2.3