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

---
 plugins/funind/invfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 439274240f..ad11f853ca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -351,7 +351,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
 	      Locusops.onConcl);
 	    observe_tac ("toto ") tclIDTAC;
     
-	    (* introducing the the result of the graph and the equality hypothesis *)
+            (* introducing the result of the graph and the equality hypothesis *)
 	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
-- 
cgit v1.2.3