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

19 files changed, 43 insertions, 43 deletions

diff --git a/doc/common/styles/html/coqremote/modules/system/system.css b/doc/common/styles/html/coqremote/modules/system/system.css
index 9371bb479e..9556c7882a 100644
--- a/doc/common/styles/html/coqremote/modules/system/system.css
+++ b/doc/common/styles/html/coqremote/modules/system/system.css
@@ -327,7 +327,7 @@ html.js fieldset.collapsed legend a {
 * html.js fieldset.collapsed table * {
   display: inline;
 }
-/* For Safari 2 to prevent collapsible fieldsets containing tables from dissapearing due to tableheader.js. */
+/* For Safari 2 to prevent collapsible fieldsets containing tables from disappearing due to tableheader.js. */
 html.js fieldset.collapsible {
   position: relative;
 }
diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
index 82ba45726e..f4d9e7fd5b 100644
--- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
+++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
@@ -33,7 +33,7 @@ TACTIC EXTEND collapse_hyps
 END
 
 (* More advanced examples, where automatic proof happens but
-   no tactic is being called explicitely.  The first one uses
+   no tactic is being called explicitly.  The first one uses
    type classes. *)
 VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
 | [ "Tuto3_3" int(n) ] -> { example_classes n }
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:
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index cc2c43e7dd..701c62cdce 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -186,7 +186,7 @@ Coq is now continuously tested against OCaml trunk, in addition to the
 oldest supported and latest OCaml releases.
 
 Coq's documentation for the development branch is now deployed
-continously at https://coq.github.io/doc/master/api (documentation of
+continuously at https://coq.github.io/doc/master/api (documentation of
 the ML API), https://coq.github.io/doc/master/refman (reference
 manual), and https://coq.github.io/doc/master/stdlib (documentation of
 the standard library). Similar links exist for the `v8.10` branch.
@@ -665,7 +665,7 @@ changes:
   - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by
     Matthieu Sozeau, for controlling the opacity status of variables and
     constants in hint databases. It is recommended to always use these
-    commands after creating a hint databse with :cmd:`Create HintDb`.
+    commands after creating a hint database with :cmd:`Create HintDb`.
 
   - Multiple sections with the same name are now allowed, by Jasper
     Hugunin.
@@ -892,7 +892,7 @@ Vernacular Commands
   `Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
 - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting
   globally the opacity flag of variables and constants in hint databases,
-  overwritting the opacity set of the hint database.
+  overwriting the opacity set of the hint database.
 - Added generic syntax for "attributes", as in:
   `#[local] Lemma foo : bar.`
 - Added the `Numeral Notation` command for registering decimal numeral
@@ -1129,7 +1129,7 @@ Tactics
   few rare incompatibilities (it was unintendedly recursively
   rewriting in the side conditions generated by H).
 - Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure
-  properties of the executation of a tactic without keeping the effect
+  properties of the execution of a tactic without keeping the effect
   of the execution.
 - `vm_compute` now supports existential variables.
 - Calls to `shelve` and `give_up` within calls to tactic `refine` now working.
@@ -1262,7 +1262,7 @@ Tools
 Tactic language
 
 - The undocumented "nameless" forms `fix N`, `cofix` have been
-  deprecated; please use `fix ident N /cofix ident` to explicitely
+  deprecated; please use `fix ident N /cofix ident` to explicitly
   name the (co)fixpoint hypothesis to be introduced.
 
 Documentation
@@ -2953,7 +2953,7 @@ Other bugfixes
 - Fix incorrect behavior of CS resolution
 - #4591: Uncaught exception in directory browsing.
 - CoqIDE is more resilient to initialization errors.
-- #4614: "Fully check the document" is uninterruptable.
+- #4614: "Fully check the document" is uninterruptible.
 - Try eta-expansion of records only on non-recursive ones
 - Fix bug when a sort is ascribed to a Record
 - Primitive projections: protect kernel from erroneous definitions.
@@ -3442,7 +3442,7 @@ Libraries
 
   * all functions over type Z : Z.add, Z.mul, ...
   * the minimal proofs of specifications for these functions : Z.add_0_l, ...
-  * an instantation of all derived properties proved generically in Numbers :
+  * an instantiation of all derived properties proved generically in Numbers :
     Z.add_comm, Z.add_assoc, ...
 
   A large part of ZArith is now simply compatibility notations, for instance
@@ -4623,7 +4623,7 @@ Setoid rewriting
   + Setoid_Theory is now an alias to Equivalence, scripts building objects
     of type Setoid_Theory need to unfold (or "red") the definitions
     of Reflexive, Symmetric and Transitive in order to get the same goals
-    as before. Scripts which introduced variables explicitely will not break.
+    as before. Scripts which introduced variables explicitly will not break.
 
   + The order of subgoals when doing [setoid_rewrite] with side-conditions
     is always the same: first the new goal, then the conditions.
@@ -5022,7 +5022,7 @@ Syntax
 
 Language and commands
 
-- Added sort-polymorphism for definitions in Type (but finally abandonned).
+- Added sort-polymorphism for definitions in Type (but finally abandoned).
 - Support for implicit arguments in the types of parameters in
   (co-)fixpoints and (co-)inductive declarations.
 - Improved type inference: use as much of possible general information.
@@ -5251,7 +5251,7 @@ Library
 
 - New file about the factorial function in Arith
 
-- An additional elimination Acc_iter for Acc, simplier than Acc_rect.
+- An additional elimination Acc_iter for Acc, simpler than Acc_rect.
   This new elimination principle is used for definition well_founded_induction.
 
 - New library NArith on binary natural numbers
@@ -5336,7 +5336,7 @@ Bugs
 Miscellaneous
 
 - Implicit parameters of inductive types definition now taken into
-  account for infering other implicit arguments
+  account for inferring other implicit arguments
 
 Incompatibilities
 
@@ -5417,7 +5417,7 @@ Gallina
 Known problems of the automatic translation
 
 - iso-latin-1 characters are no longer supported: move your files to
-  7-bits ASCII or unicode before translation (swith to unicode is
+  7-bits ASCII or unicode before translation (switch to unicode is
   automatically done if a file is loaded and saved again by coqide)
 - Renaming in ZArith: incompatibilities in Coq user contribs due to
   merging names INZ, from Reals, and inject_nat.
@@ -5442,7 +5442,7 @@ Vernacular commands
 - "Functional Scheme" and "Functional Induction" extended to polymorphic
   types and dependent types
 - Notation now allows recursive patterns, hence recovering parts of the
-  fonctionalities of pre-V8 Grammar/Syntax commands
+  functionalities of pre-V8 Grammar/Syntax commands
 - Command "Print." discontinued.
 - Redundant syntax "Implicit Arguments On/Off" discontinued
 
diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst
index 0f5b991ba4..c4a48d6985 100644
--- a/doc/sphinx/history.rst
+++ b/doc/sphinx/history.rst
@@ -110,7 +110,7 @@ advantage of special hardware, debuggers, and the like. We hope that |Coq|
 can be of use to researchers interested in experimenting with this new
 methodology.
 
-.. [#years] At the time of writting, i.e. 1995.
+.. [#years] At the time of writing, i.e. 1995.
 
 Versions 1 to 5
 ---------------
@@ -305,7 +305,7 @@ Michel Mauny, Ascander Suarez and Pierre Weis.
 V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
 November 1986. V3.4 was developed in the first half of 1987.
 
-Thierry Coquand held a post-doctoral position in Cambrige University
+Thierry Coquand held a post-doctoral position in Cambridge University
 in 1986-87, where he developed a variant implementation in SML, with
 which he wrote some developments on fixpoints in Scott's domains.
 
@@ -345,7 +345,7 @@ lemmas when local hypotheses of proofs were discharged. This gave a
 notion of global mathematical environment with local sections.
 
 Another significant practical change was that the system, originally
-developped on the VAX central computer of our lab, was transferred on
+developed on the VAX central computer of our lab, was transferred on
 SUN personal workstations, allowing a level of distributed
 development.  The extraction algorithm was modified, with three
 annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop``
@@ -503,7 +503,7 @@ of CNRS-ENS Lyon.
 Chetan Murthy joined the team in 1991 and became the main software
 architect of Version 5. He completely rehauled the implementation for
 efficiency.  Versions 5.6 and 5.8 were major distributed versions,
-with complete documentation and a library of users' developements. The
+with complete documentation and a library of users' developments. The
 use of the RCS revision control system, and systematic ChangeLog
 files, allow a more precise tracking of the software developments.
 
@@ -1330,7 +1330,7 @@ Language
 
 - Inductive definitions now accept ">" in constructor types to declare
   the corresponding constructor as a coercion.
-- Idem for assumptions declarations and constants when the type is mentionned.
+- Idem for assumptions declarations and constants when the type is mentioned.
 - The "Coercion" and "Canonical Structure" keywords now accept the
   same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t".
 - Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u".
@@ -1383,7 +1383,7 @@ Tactics
   it can also recognize 'False' in the hypothesis and use it to solve the
   goal.
 - Coercions now handled in "with" bindings
-- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses
+- "Subst x" replaces all occurrences of x by t in the goal and hypotheses
   when an hypothesis x=t or x:=t or t=x exists
 - Fresh names for Assert and Pose now based on collision-avoiding
   Intro naming strategy (exceptional source of incompatibilities)
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index bbd7e0ba3d..fed7111628 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -708,7 +708,7 @@ tactic
       for printing.
 
    By copying the definition of :tacn:`time_constr` from the standard library,
-   users can achive support for a fixed pattern of nesting by passing
+   users can achieve support for a fixed pattern of nesting by passing
    different :token:`string` parameters to :tacn:`restart_timer` and
    :tacn:`finish_timing` at each level of nesting.
 
@@ -1676,7 +1676,7 @@ It is possible to measure the time spent in invocations of primitive
 tactics as well as tactics defined in |Ltac| and their inner
 invocations. The primary use is the development of complex tactics,
 which can sometimes be so slow as to impede interactive usage. The
-reasons for the performence degradation can be intricate, like a slowly
+reasons for the performance degradation can be intricate, like a slowly
 performing |Ltac| match or a sub-tactic whose performance only
 degrades in certain situations. The profiler generates a call tree and
 indicates the time spent in a tactic depending on its calling context. Thus
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 75e019592f..b19b0742c1 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -853,7 +853,7 @@ An *occurrence switch* can be:
   algorithm in a local definition, instead of copying large terms by
   hand.
 
-It is important to remember that matching *preceeds* occurrence
+It is important to remember that matching *precedes* occurrence
 selection.
 
   .. example::
@@ -2455,7 +2455,7 @@ the holes are abstracted in term.
      Lemma test : True.
      have: _ * 0 = 0.
 
-  The invokation of ``have`` is equivalent to:
+  The invocation of ``have`` is equivalent to:
 
   .. coqtop:: reset none
 
@@ -4927,7 +4927,7 @@ bookkeeping steps.
      apply/PQequiv.
 
   thus in this case, the tactic ``apply/PQequiv`` is equivalent to
-  ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is tha analogue of
+  ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is the analogue of
   ``iffRL`` for the converse implication.
 
 Any |SSR| term whose type coerces to a double implication can be
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4e47621938..2ee23df019 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3714,7 +3714,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. cmdv:: Hint Resolve -> @term : @ident
 
       Adds the left-to-right implication of an equivalence as a hint (informally
-      the hint will be used as :n:`apply <- @term`, although as mentionned
+      the hint will be used as :n:`apply <- @term`, although as mentioned
       before, the tactic actually used is a restricted version of
       :tacn:`apply`).
 
@@ -3783,7 +3783,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
       This sets the transparency flag used during unification of
       hints in the database for all constants or all variables,
-      overwritting the existing settings of opacity. It is advised
+      overwriting the existing settings of opacity. It is advised
       to use this just after a :cmd:`Create HintDb` command.
 
    .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index cda228a7da..6da42f4a48 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1198,7 +1198,7 @@ The ``function_scope`` interpretation scope
 
 The scope ``function_scope`` also has a special status.
 It is temporarily activated each time the argument of a global reference is
-recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or
+recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or
 :g:`A -> B`.
 
 
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index d8ac640f2a..dde8a7b838 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -412,7 +412,7 @@ but its behaviour is not to fold the abbreviation at all.}.
 {\tt LetTac} could be followed by a specification (called a clause) of
 the places where the abbreviation had to be folded (hypothese and/or
 conclusion). Clauses are the syntactic notion to denote in which parts
-of a goal a given transformation shold occur. Its basic notation is
+of a goal a given transformation should occur. Its basic notation is
 either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |-
 \textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all
 the hypotheses), or a comma-separated list of either hypothesis name,
@@ -620,7 +620,7 @@ These constraints are met by the makefiles produced by {\tt coq\_makefile}
 
 Otherwise, modify your build program so as to pass option {\tt
 -translate} to program {\tt coqc}. The effect of this option is to
-ouptut the translated source of any {\tt .v} file in a file with
+output the translated source of any {\tt .v} file in a file with
 extension {\tt .v8} located in the same directory than the original
 file.
 
@@ -675,7 +675,7 @@ solve all occurrences of the problem.
 The definition of identifiers changed. Most of those changes are
 handled by the translator. They include:
 \begin{itemize}
-\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt
+\item {\tt \_} is not an identifier anymore: it is translated to {\tt
 x\_}
 \item avoid clash with new keywords by adding a trailing {\tt \_}
 \end{itemize}
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index 1de9890992..ba58ff0084 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -52,7 +52,7 @@ def is_whitespace_string(elem):
     return isinstance(elem, NavigableString) and elem.strip() == ""
 
 def strip_soup(soup, pred):
-    """Strip elements maching pred from front and tail of soup."""
+    """Strip elements matching pred from front and tail of soup."""
     while soup.contents and pred(soup.contents[-1]):
         soup.contents.pop()
 
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index 26f6255069..2b124ee5c1 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -47,7 +47,7 @@ class CoqTop:
         :param coqtop_bin: The path to coqtop; uses $COQBIN by default, falling back to "coqtop"
         :param color:      When True, tell coqtop to produce ANSI color codes (see
                            the ansicolors module)
-        :param args:       Additional arugments to coqtop.
+        :param args:       Additional arguments to coqtop.
         """
         self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
         if not pexpect.utils.which(self.coqtop_bin):
@@ -68,7 +68,7 @@ class CoqTop:
         self.coqtop.kill(9)
 
     def next_prompt(self):
-        """Wait for the next coqtop prompt, and return the output preceeding it."""
+        """Wait for the next coqtop prompt, and return the output preceding it."""
         self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10)
         return self.coqtop.before
 
diff --git a/doc/whodidwhat/whodidwhat-8.2update.tex b/doc/whodidwhat/whodidwhat-8.2update.tex
index 4f4f0e952e..f45e6564f2 100644
--- a/doc/whodidwhat/whodidwhat-8.2update.tex
+++ b/doc/whodidwhat/whodidwhat-8.2update.tex
@@ -181,7 +181,7 @@
 \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
 \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
 \item Searching: Hugo Herbelin, Yves Bertot
-\item Whelp suppport: Hugo Herbelin
+\item Whelp support: Hugo Herbelin
 \end{itemize}
 
 \section{Parsing and printing}
diff --git a/doc/whodidwhat/whodidwhat-8.3update.tex b/doc/whodidwhat/whodidwhat-8.3update.tex
index 0a07378169..7cce0083d5 100644
--- a/doc/whodidwhat/whodidwhat-8.3update.tex
+++ b/doc/whodidwhat/whodidwhat-8.3update.tex
@@ -188,7 +188,7 @@
 \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
 \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
 \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
-\item Whelp suppport: Hugo Herbelin
+\item Whelp support: Hugo Herbelin
 \end{itemize}
 
 \section{Parsing and printing}
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex
index bb4c5ce469..2d74a653ed 100644
--- a/doc/whodidwhat/whodidwhat-8.4update.tex
+++ b/doc/whodidwhat/whodidwhat-8.4update.tex
@@ -191,7 +191,7 @@
 \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
 \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
 \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
-\item Whelp suppport: Hugo Herbelin
+\item Whelp support: Hugo Herbelin
 \end{itemize}
 
 \section{Parsing and printing}
diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex
index ce099dc363..600ecf93db 100644
--- a/doc/whodidwhat/whodidwhat-8.5update.tex
+++ b/doc/whodidwhat/whodidwhat-8.5update.tex
@@ -197,7 +197,7 @@
 \item Options management: Hugo Herbelin with contributions by Arnaud Spiwack
 \item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
 \item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
-\item Whelp suppport: Hugo Herbelin
+\item Whelp support: Hugo Herbelin
 \end{itemize}
 
 \section{Parsing and printing}