Fix #8251: remove "the the" occurrences

1 files changed, 1 insertions, 1 deletions

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.                 *)