Merge PR coq#18356: Fix typo in documentation

Reviewed-by: proux01 Co-authored-by: proux01 <proux01@users.noreply.github.com>
Villetaneuse · Nov 30, 2023 · 1788628 · 1788628
2 parents d98e511 + 15a8e8a
commit 1788628
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
@@ -159,7 +159,7 @@ One can define new types with the following commands.
       tac2rec_field ::= {? mutable } @ident : @ltac2_type
 
    :n:`:=`
-     Defines a type with with an explicit set of constructors
+     Defines a type with an explicit set of constructors
 
    :n:`::=`
      Extends an existing open variant type, a special kind of variant type whose constructors are not

diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
@@ -332,7 +332,7 @@ Register protect_term as plugins.ssreflect.protect_term.
   - unkeyed t will match any subterm that unifies with t, regardless of
     whether it displays the same head symbol as t.
   - unkeyed t a b will match any application of a term f unifying with t,
-    to two arguments unifying with with a and b, respectively, regardless of
+    to two arguments unifying with a and b, respectively, regardless of
     apparent head symbols.
   - unkeyed x where x is a variable will match any subterm with the same
     type as x (when x would raise the 'indeterminate pattern' error).        **)