Merge PR #8296: Fix #8251: remove "the the" occurrences

9 files changed, 9 insertions, 9 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 1643baf0e8..2264b170fc 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -303,7 +303,7 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
        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:`@…```.
 
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 0f51b3eba3..88da58c27d 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -107,7 +107,7 @@ and ``coqtop``, unless stated otherwise:
   to the OCaml loadpath. See also: :ref:`names-of-libraries` and the
   command Declare ML Module Section :ref:`compiled-files`.
 :-Q *directory* dirpath: Add physical path *directory* to the list of
-  directories where |Coq| looks for a file and bind it to the the logical
+  directories where |Coq| looks for a file and bind it to the logical
   directory *dirpath*. The subdirectory structure of *directory* is
   recursively available from |Coq| using absolute names (extending the
   dirpath prefix) (see Section :ref:`qualified-names`).Note that only those
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 6fbb2fac6d..0310dbead5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -391,7 +391,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    focused goal independently and stops if it succeeds; otherwise it
    tries to apply :n:`v__2` and so on. It fails when there is no
    applicable tactic. In other words,
-   :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first
+   :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the first
    :n:`v__i` to have *at least* one success.
 
    .. exn:: No applicable tactic.
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:`@…```.
     """
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)));
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 7143f51853..d5d36c97fa 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -41,7 +41,7 @@ val register_alias : alias -> alias_tactic -> unit
 (** Register a tactic alias. *)
 
 val interp_alias : alias -> alias_tactic
-(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+(** Recover the body of an alias. Raises an anomaly if it does not exist. *)
 
 val check_alias : alias -> bool
 (** Returns [true] if an alias is defined, false otherwise. *)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 54f3f9c718..1f3c758e5c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -469,7 +469,7 @@ let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
 (* term mkApp (t', args) is convertible to t.                        *)
 (* This makes a useful shorthand for local definitions in proofs,    *)
 (* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *)
-(* and, in context of the the 4CT library, pose mid := maps id means *)
+(* and, in context of the 4CT library, pose mid := maps id means *)
 (*    pose mid := fun d : detaSet => @maps d d (@id (datum d))       *)
 (* Note that this facility does not extend to set, which tries       *)
 (* instead to fill holes by matching a goal subterm.                 *)
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
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 =