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

---
 vernac/auto_ind_decl.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ee578669c2..e33aa38173 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let destruct_ind sigma c =
   then avoid should be
  [| lb_An ... lb _A1  (resp. bl_An ... bl_A1)
     eq_An .... eq_A1 An ... A1 |]
-so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
+so from Ai we can find the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
 let do_replace_lb mode lb_scheme_key aavoid narg p q =
-- 
cgit v1.2.3