Merge PR #10203: Fixing typos - Part 1

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: gares
Reviewed-by: jfehrle
Reviewed-by: vbgl

4 files changed, 4 insertions, 4 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 8a895eb515..3dc8707a34 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -168,7 +168,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
 
 .. cmd:: Extraction NoInline {+ @qualid }
 
-   Conversely, the constants mentionned by this command will
+   Conversely, the constants mentioned by this command will
    never be inlined during extraction.
 
 .. cmd:: Print Extraction Inline
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 847abb33fc..68f6d4008a 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -441,7 +441,7 @@ First class setoids and morphisms
 The implementation is based on a first-class representation of
 properties of relations and morphisms as typeclasses. That is, the
 various combinations of properties on relations and morphisms are
-represented as records and instances of theses classes are put in a
+represented as records and instances of these classes are put in a
 hint database. For example, the declaration:
 
 .. coqdoc::
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 65934efaa6..2ba13db042 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -385,7 +385,7 @@ few other commands related to typeclasses.
 
      .. note::
         As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully
-        mimicks what happens during typeclass resolution when it is called
+        mimics what happens during typeclass resolution when it is called
         during refinement/type inference, except that *only* declared class
         subgoals are considered at the start of resolution during type
         inference, while ``all`` can select non-class subgoals as well. It might
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 6b10b7c0b3..1aa2111816 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -449,7 +449,7 @@ underscore or by omitting the annotation to a polymorphic definition.
    This option, on by default, removes universes which appear only in
    the body of an opaque polymorphic definition from the definition's
    universe arguments. As such, no value needs to be provided for
-   these universes when instanciating the definition. Universe
+   these universes when instantiating the definition. Universe
    constraints are automatically adjusted.
 
    Consider the following definition: