Fixing typos - Part 1

61 files changed, 107 insertions, 107 deletions

diff --git a/.mailmap b/.mailmap
index 18155a3d28..07e9f70bc9 100644
--- a/.mailmap
+++ b/.mailmap
@@ -6,7 +6,7 @@
 ## To avoid spam issues, we use by default a pseudo-email <login@gforge>
 ## for all persons that haven't made commits with real emails
 ##
-## If you're mentionned here and want to update your information,
+## If you're mentioned here and want to update your information,
 ## either amend this file and commit it, or contact the coqdev list
 
 Abhishek Anand <abhishek.anand.iitg@gmail.com>     Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com>
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 31fa3d2c4a..e811c116b6 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -31,7 +31,7 @@ account). You can file a bug for any of the following:
 It would help if you search the existing issues before reporting a bug. This
 can be difficult, so consider it extra credit. We don't mind duplicate bug
 reports. If unsure, you are always very welcome to ask on our [Discourse forum][]
-or [Gitter chat][] before, after, or while writting a bug report
+or [Gitter chat][] before, after, or while writing a bug report
 
 When it applies, it's extremely helpful for bug reports to include sample
 code, and much better if the code is self-contained and complete. It's not
diff --git a/Makefile.build b/Makefile.build
index 034c9ea03c..147668187f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -150,7 +150,7 @@ endif
 
 ###########################################################################
 
-# This include below will lauch the build of all .d.
+# This include below will launch the build of all .d.
 # The - at front is for disabling warnings about currently missing ones.
 # For creating the missing .d, make will recursively build things like
 # coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d).
diff --git a/Makefile.dev b/Makefile.dev
index 13b85dfad4..6057696375 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -8,7 +8,7 @@
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
 
-# Extra targets for developpers :
+# Extra targets for developers :
 # debug printers, revision, partial targets ...
 
 #########################
diff --git a/Makefile.doc b/Makefile.doc
index 25d146000b..94642e702f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -167,7 +167,7 @@ doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li
 	$(PDFLATEX) -interaction=batchmode Library;\
 	../tools/show_latex_messages -no-overfull Library.log)
 
-### Standard library (full version if you're crazy enouth to try)
+### Standard library (full version if you're crazy enough to try)
 
 doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex
 	sed -e 's/Library.coqdoc/FullLibrary.coqdoc/g;s/\\begin{document}/\\newcommand{\\textlambda}{\\ensuremath{\\lambda}}\\newcommand{\\textPi}{\\ensuremath{\\Pi}}\\begin{document}/' $< > $@
diff --git a/Makefile.dune b/Makefile.dune
index ebf74978a9..88055d62dc 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -5,7 +5,7 @@
 .PHONY: coq coqide coqide-server                      # Package targets
 .PHONY: quickbyte quickopt quickide                   # Partial / quick developer targets
 .PHONY: refman-html stdlib-html apidoc                # Documentation targets
-.PHONY: test-suite release                            # Accesory targets
+.PHONY: test-suite release                            # Accessory targets
 .PHONY: ocheck trunk ireport clean                    # Maintenance targets
 
 # use DUNEOPT=--display=short for a more verbose build
diff --git a/Makefile.ide b/Makefile.ide
index 4cec7aa443..89c1f246db 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -77,7 +77,7 @@ ADWAITASHARE=$(shell ls -d /usr/local/Cellar/adwaita-icon-theme/*)/share
 .PHONY: coqide coqide-opt coqide-byte coqide-bindings coqide-files coqide-binaries
 .PHONY: ide-toploop ide-byteloop ide-optloop
 
-# target to build CoqIde (native version) and the stuff needed to lauch it
+# target to build CoqIde (native version) and the stuff needed to launch it
 coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) $(TOPBIN)
 
 # target to build CoqIde (in native and byte versions), and no more
diff --git a/checker/include b/checker/include
index 3ffc301724..411321cb3e 100644
--- a/checker/include
+++ b/checker/include
@@ -3,7 +3,7 @@
 (* Caml script to include for debugging the checker.
    Usage: from the checker/ directory launch ocaml toplevel and then
    type #use"include";;
-   This command loads the relevent modules, defines some pretty
+   This command loads the relevant modules, defines some pretty
    printers, and provides functions to interactively check modules
    (mainly run_l and norec).
  *)
diff --git a/clib/iStream.mli b/clib/iStream.mli
index 40d579be60..e56f066c5e 100644
--- a/clib/iStream.mli
+++ b/clib/iStream.mli
@@ -31,7 +31,7 @@ val cons : 'a -> 'a t -> 'a t
 (** Append an element in front of a stream. *)
 
 val thunk : (unit -> ('a,'a t) u) -> 'a t
-(** Internalize the lazyness of a stream. *)
+(** Internalize the laziness of a stream. *)
 
 val make : ('a -> ('b, 'a) u) -> 'a -> 'b t
 (** Coiteration constructor. *)
diff --git a/configure.ml b/configure.ml
index 57f31fec4c..3ced82718e 100644
--- a/configure.ml
+++ b/configure.ml
@@ -451,7 +451,7 @@ let coq_profile_flag = if !prefs.profile then "-p" else ""
 let coq_annot_flag = if !prefs.annot then "-annot" else ""
 let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else ""
 
-(* This variable can be overriden only for debug purposes, use with
+(* This variable can be overridden only for debug purposes, use with
    care. *)
 let coq_safe_string = "-safe-string"
 let coq_strict_sequence = "-strict-sequence"
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 26e1e25fb9..42fe13e4eb 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -499,7 +499,7 @@ let print_rules fmt (name, rules) =
   let pr fmt l = print_list fmt (fun fmt r -> fprintf fmt "(%a)" GramExt.print_extrule r) l in
   match rules with
   | [([SymbEntry (e, None)], [Some s], { code = c } )] when String.trim c = s ->
-    (* This is a horrible hack to work aroud limitations of camlp5 regarding
+    (* This is a horrible hack to work around limitations of camlp5 regarding
        factorization of parsing rules. It allows to recognize rules of the
        form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and
        reuse the same entry directly. *)
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index c3f3a97ff5..7c8f73c7e4 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -285,9 +285,9 @@ SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
 SET TARGET_ARCH=%ARCH%-w64-mingw32

 SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash

 

-REM Convert pathes to various formats

+REM Convert paths to various formats

 REM WFMT = windows format (C:\..)          Used in this batch file.

-REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH varible, which is : separated, so C: doesn't work.

+REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH variable, which is : separated, so C: doesn't work.

 REM MFMT = MinGW format (C:/...)           Used for the build, because \\ requires escaping. Mingw can handle \ and /.

 

 SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%

@@ -429,13 +429,13 @@ ECHO ========== BATCH FUNCTIONS ==========
   REM  01234567890123456789012345678901234567890123456789012345678901234567890123456789

   ECHO -arch     ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit

   ECHO -mode     ^<mingwincygwin = install coq in default cygwin mingw sysroot^>

-  ECHO           ^<absoloute = install coq in -destcoq absulute path^>

+  ECHO           ^<absolute = install coq in -destcoq absolute path^>

   ECHO           ^<relocatable = install relocatable coq in -destcoq path^>

   ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)

   ECHO -ocaml    ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)

   ECHO -make     ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)

   ECHO -destcyg  ^<path to cygwin destination folder^>

-  ECHO -destcoq  ^<path to coq destination folder (mode=absoloute/relocatable)^>

+  ECHO -destcoq  ^<path to coq destination folder (mode=absolute/relocatable)^>

   ECHO -setup    ^<cygwin setup program name^> (auto adjusted to -arch)

   ECHO -proxy    ^<internet proxy^>

   ECHO -cygrepo  ^<cygwin download repository^>

diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index a392115ea4..55b46c616c 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -43,7 +43,7 @@ paths like "C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys
 DLL.
 
 The missing piece is a posix shell running on plain Windows (without msys or
-Cygwin DLL) and not beeing a binary from obscure sources. I am working on it ...
+Cygwin DLL) and not being a binary from obscure sources. I am working on it ...
 
 Since compiling gcc and binutils takes a while and it is not of much use without
 a shell, the building of these components is currently disabled. OCaml is built
@@ -274,11 +274,11 @@ Default value: N
 
 ===== -cygquiet =====
 
-Control if the Cygwin setup runs quitely or interactive.
+Control if the Cygwin setup runs quietly or interactive.
 
 Possible values:
 
-Y: Install Cygwin quitely without user interaction.
+Y: Install Cygwin quietly without user interaction.
 
 N: Install Cygwin interactively (allows to select additional packages).
 
@@ -344,12 +344,12 @@ selecting more packages)
 ==================== TODO ====================
 
 - Check for spaces in destination paths
-- Check for = signs in all paths (DOS commands don't work with pathes with = in it, possibly even when quoted)
+- Check for = signs in all paths (DOS commands don't work with paths with = in it, possibly even when quoted)
 - Installer doesn't remove OCAMLLIB environment variables (it is in the script, but doesn't seem to work)
 - CoqIDE doesn't find theme files
 - Finish / test mingw_in_Cygwin mode (coqide doesn't start, coqc slow cause of scanning complete share folder)
-- Possibly create/login as specific user to bash (not sure if it makes sense - nead to create additional bash login link then)
-- maybe move share/doc/menhir somehwere else (reduces coqc startup time)
+- Possibly create/login as specific user to bash (not sure if it makes sense - need to create additional bash login link then)
+- maybe move share/doc/menhir somewhere else (reduces coqc startup time)
 - Use original installed file list for removing files in uninstaller 
 
 ==================== Issues with relocation ====================
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
index 3bba451ec6..543ca972cd 100644
--- a/dev/build/windows/difftar-folder.sh
+++ b/dev/build/windows/difftar-folder.sh
@@ -40,7 +40,7 @@ fi
 # Get path prefix if --strip is used
 
 if [ "$strip" -gt 0 ] ; then
-  # Get the path/name of the first file from teh tar and extract the first $strip path components
+  # Get the path/name of the first file from the tar and extract the first $strip path components
   # This assumes that the first file in the tar file has at least $strip many path components
   prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/
 else
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index d737632638..549f70e8fe 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -765,7 +765,7 @@ function make_ncurses {
   # gettext make/make install work anyway
   #
   # CONFIGURE PARAMETERS
-  # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW)
+  # --enable-term-driver --enable-sp-funcs is required for mingw (see README.MinGW)
   # additional changes
   # ADD --with-pkg-config
   # ADD --enable-pc-files
@@ -1281,7 +1281,7 @@ function copy_coq_objects {
   done
 }
 
-# Copy required GTK config and suport files
+# Copy required GTK config and support files
 
 function copy_coq_gtk {
   echo 'gtk-theme-name = "Default"'     >  "$PREFIX/etc/gtk-3.0/gtkrc"
diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c
index e4fdcd4d7d..c4c7ec2bff 100755
--- a/dev/build/windows/patches_coq/pkg-config.c
+++ b/dev/build/windows/patches_coq/pkg-config.c
@@ -1,5 +1,5 @@
 // MinGW personality wrapper for pkgconf
-// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config
+// This is an executable replacement for the shell scripts /bin/ARCH-pkg-config
 // Compile with e.g.
 // gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe
 // gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 98ea594366..408d36df7f 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -31,7 +31,7 @@ PR by running GitLab CI on your private branches. To do so follow these steps:
 6. You are encouraged to go to the CI / CD general settings and increase the
    timeout from 1h to 2h for better reliability.
 
-Now everytime you push (including force-push unless you changed the default
+Now every time you push (including force-push unless you changed the default
 GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and
 CI will be run. You will receive an e-mail with a report of the failures if
 there are some.
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index c9eceb1270..66f5a96802 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -92,7 +92,7 @@ When fixes are ready, there are two cases to consider:
 Once all reviewers approved the PR, the assignee is expected to check that CI
 completed without relevant failures, and that the PR comes with appropriate
 documentation and test cases. If not, they should leave a comment on the PR and
-put the approriate label. Otherwise, they are expected to merge the PR using the
+put the appropriate label. Otherwise, they are expected to merge the PR using the
 [merge script](../tools/merge-pr.sh).
 
 When CI has a few failures which look spurious, restarting the corresponding
diff --git a/dev/doc/archive/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex
index 0b0811d81b..8b0b14efb8 100644
--- a/dev/doc/archive/naming-conventions.tex
+++ b/dev/doc/archive/naming-conventions.tex
@@ -570,11 +570,11 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}.
 Zero on domain {\D} & D0 & (notation \verb=0=)\\
 One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\
 Successor on domain {\D} & Dsucc\\
-Predessor on domain {\D} & Dpred\\
-Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}}
+Predecessor on domain {\D} & Dpred\\
+Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existing libraries that already use \texttt{plus} and \texttt{mult}}
  & (infix notation \verb=+= [50,L])\\
 Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\
-Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\
+Subtraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\
 Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\
 Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\
 Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\
diff --git a/dev/doc/archive/versions-history.tex b/dev/doc/archive/versions-history.tex
index 25dabad497..46516dd4e4 100644
--- a/dev/doc/archive/versions-history.tex
+++ b/dev/doc/archive/versions-history.tex
@@ -372,7 +372,7 @@ Coq V8.4pl5& released 22 October 2014 & \\
 Coq V8.4pl6& released 9 April 2015 & \\
 
 Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\
-&& \feature{asynchonous evaluation} [8-8-2013]\\
+&& \feature{asynchronous evaluation} [8-8-2013]\\
 && \feature{new proof engine deployed} [2-11-2013]\\
 && \feature{universe polymorphism} [6-5-2014]\\
 && \feature{primitive projections} [6-5-2014]\\
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index b0a2b04121..6efc8ec1fe 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -9,13 +9,13 @@ HISTORY:
 
 * March 2010 (Pierre Letouzey).
   Revised build system. In particular, no more stage1,2,3 :
-  - Stage3 was removed some time ago when coqdep was splitted into
+  - Stage3 was removed some time ago when coqdep was split into
     coqdep_boot and full coqdep.
   - Stage1,2 were replaced by brutal inclusion of all .d at the start
     of Makefile.build, without trying to guess what could be done at
     what time. Some initial inclusions hence _fail_, but "make" tries
     again later and succeed.
-  - Btw, .ml4 are explicitely turned into .ml files, which stay after build.
+  - Btw, .ml4 are explicitly turned into .ml files, which stay after build.
     By default, they are in binary ast format, see READABLE_ML4 option.
 
 * February 2014 (Pierre Letouzey).
@@ -87,7 +87,7 @@ Cons:
    clear-text generated .ml.
 
 
-Makefiles hierachy
+Makefiles hierarchy
 ------------------
 
 The Makefile is separated in several files :
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 8cefe699cc..1ad649bc94 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -18,8 +18,8 @@ See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types
 * Annotation before commands: +/-/@
 
 a command starting by - is always successful (errors are ignored)
-a command starting by + is runned even if option -n is given to make
-a command starting by @ is not echoed before being runned
+a command starting by + is ran even if option -n is given to make
+a command starting by @ is not echoed before being ran
 
 * Custom functions
 
@@ -36,7 +36,7 @@ If the file given to -include doesn't exist, make tries to build it,
 and even retries again if necessary, but doesn't care if this build
 finally fails. We used to rely on this "feature", but this should not
 be the case anymore. We kept "-include" instead of "include" for
-avoiding warnings about initially non-existant files.
+avoiding warnings about initially non-existent files.
 
 Changes (for old-timers)
 ------------------------
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7221c3de56..339ac2d9b7 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1278,7 +1278,7 @@ next_global_ident_away true -> next_ident_away_in_goal
 next_global_ident_away false -> next_global_ident_away
 ```
 
-### Cleaning in commmand.ml
+### Cleaning in command.ml
 
 Functions about starting/ending a lemma are in lemmas.ml
 Functions about inductive schemes are in indschemes.ml
@@ -1593,7 +1593,7 @@ Other kinds of objects:
 
 #### Writing subst_thing functions
 
-The subst_thing shoud not copy the thing if it hasn't actually
+The subst_thing should not copy the thing if it hasn't actually
 changed. There are some cool emacs macros in dev/objects.el 
 to help writing subst functions this way quickly and without errors.
 Also there are *_smartmap functions in Util.
diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md
index bb17e8fb62..16abf3f519 100644
--- a/dev/doc/econstr.md
+++ b/dev/doc/econstr.md
@@ -25,7 +25,7 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter
 Essentially, each time it sees an evar which happens to be defined in the
 provided evar-map, it replaces it with the corresponding body and carries on.
 
-Due to universe unification occuring at the tactic level, the same goes for
+Due to universe unification occurring at the tactic level, the same goes for
 universe instances and sorts. See the `ESort` and `EInstance` modules in
 `EConstr`.
 
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index 774552237a..a2c8d2f5ac 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -121,7 +121,7 @@ a limited set of derivation rules), it is recommended to generate proofs as
 much as possible by refining in ML tactics when it is possible and easy enough.
 Indeed, this prevents dependence on fragile constructions such as unification.
 
-Obviously, it does not forbid the use of tacticals to mimick what one would do
+Obviously, it does not forbid the use of tacticals to mimic what one would do
 in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple
 semantics. A list of such tacticals can be found in the `Tacticals` module. Most
 of them are a porting of the tacticals from the old engine to the new one, so
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 189d6f9fa5..452160ea5a 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -113,7 +113,7 @@
 - [ ] Upload the new version of the reference manual to the website.
   *TODO: setup some continuous deployment for this.*
 - [ ] Merge the website update, publish the release
-  and send annoucement e-mails.
+  and send announcement e-mails.
 - [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
   *TODO: automate this.*
 - [ ] Close the milestone
diff --git a/dev/doc/universes.md b/dev/doc/universes.md
index c276603ed2..026c3830a2 100644
--- a/dev/doc/universes.md
+++ b/dev/doc/universes.md
@@ -163,9 +163,9 @@ only, it's just a matter of using `Evd.fresh_global` /
 The universe graph
 ------------------
 
-To accomodate universe polymorphic definitions, the graph structure in
+To accommodate universe polymorphic definitions, the graph structure in
 kernel/univ.ml was modified. The new API forces every universe to be
-declared before it is mentionned in any constraint. This forces to
+declared before it is mentioned in any constraint. This forces to
 declare every universe to be >= Set or > Set. Every universe variable
 introduced during elaboration is >= Set. Every _global_ universe is now
 declared explicitly > Set, _after_ typechecking the definition. In
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 48671c03b6..e23d1234f7 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -437,7 +437,7 @@ Searches for objects that satisfy a list of constraints. If `${positiveConstrain
 * Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string.
 * SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string.
 * In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure.
-* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*.
+* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is omitted*.
 
 -------------------------------
 
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
index d8043558eb..96c92e3162 100755
--- a/dev/lint-commits.sh
+++ b/dev/lint-commits.sh
@@ -34,6 +34,6 @@ if [ "${#bad[@]}" != 0 ]
 then
     >&2 echo "Whitespace errors!"
     >&2 echo "In commits ${bad[*]}"
-    >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
+    >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
     exit 1
 fi
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index f48013cf2e..b4c5d3d528 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -6,7 +6,7 @@
 
 ;SetCompress off
 SetCompressor lzma
-; Comment out after debuging.
+; Comment out after debugging.
 
 ; The VERSION should be passed as an argument at compile time using :
 ;
diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex
index ae4b569b36..84894b6f7c 100644
--- a/dev/v8-syntax/memo-v8.tex
+++ b/dev/v8-syntax/memo-v8.tex
@@ -55,7 +55,7 @@ _ are allowed after the first character.
 Quoted strings are used typically to give a filename (which may not
 be a regular identifier). As before they are written between double
 quotes ("). Unlike for V7, there is no escape character: characters
-are written normaly but the double quote which is doubled.
+are written normally but the double quote which is doubled.
 
 \section{Main changes in terms w.r.t. V7}
 
@@ -252,7 +252,7 @@ became \TERM{context}. Syntax is unified with subterm matching.
 
 \subsection{Occurrences}
 
-To avoid ambiguity between a numeric literal and the optionnal
+To avoid ambiguity between a numeric literal and the optional
 occurrence numbers of this term, the occurrence numbers are put after
 the term itself. This applies to tactic \TERM{pattern} and also
 \TERM{unfold}
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}
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 0a5bba39b9..7c2ecca89e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -860,7 +860,7 @@ let compare_constructor_instances evd u u' =
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extention of those in [sigma1]. *)
+    assumed to be an extension of those in [sigma1]. *)
 let eq_constr_univs_test sigma1 sigma2 t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 8eaff8bd13..907be8eba2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -208,7 +208,7 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extention of those in [sigma1]. *)
+    assumed to be an extension of those in [sigma1]. *)
 val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
 
 (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index e0c24f049f..a504ee28e2 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -151,7 +151,7 @@ struct
   (** Double-continuation backtracking monads are reasonable folklore
       for "search" implementations (including the Tac interactive
       prover's tactics). Yet it's quite hard to wrap your head around
-      these.  I recommand reading a few times the "Backtracking,
+      these.  I recommend reading a few times the "Backtracking,
       Interleaving, and Terminating Monad Transformers" paper by
       O. Kiselyov, C. Shan, D. Friedman, and A. Sabry.  The peculiar
       shape of the monadic type is reminiscent of that of the
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 5c5a02d3fa..c00c90e5e9 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -31,7 +31,7 @@ type entry = (EConstr.constr * EConstr.types) list
     ide-s. *)
 (* spiwack: the type of [proofview] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
 let proofview p =
@@ -114,7 +114,7 @@ type focus_context = goal_with_state list * goal_with_state list
     instance, ide-s. *)
 (* spiwack: the type of [focus_context] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: the goals in the context, as a "zipper" (the first
    list is in reversed order). *)
 let focus_context (left,right) =
@@ -123,7 +123,7 @@ let focus_context (left,right) =
 (** This (internal) function extracts a sublist between two indices,
     and returns this sublist together with its context: if it returns
     [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the
-    original list.  The focused list has lenght [j-i-1] and contains
+    original list.  The focused list has length [j-i-1] and contains
     the goals from number [i] to number [j] (both included) the first
     goal of the list being numbered [1].  [focus_sublist i j l] raises
     [IndexOutOfRange] if [i > length l], or [j > length l] or [j <
@@ -245,7 +245,7 @@ let tclUNIT = Proof.return
 (** Bind operation of the tactic monad. *)
 let tclBIND = Proof.(>>=)
 
-(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation,
+(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
     it's a specialized "bind". *)
 let tclTHEN = Proof.(>>)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index b7ff3ac432..60697c1611 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -24,7 +24,7 @@ type proofview
     ide-s. *)
 (* spiwack: the type of [proofview] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
 val proofview : proofview -> Evar.t list * Evd.evar_map
@@ -95,7 +95,7 @@ type focus_context
     instance, ide-s. *)
 (* spiwack: the type of [focus_context] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: the goals in the context, as a "zipper" (the first
    list is in reversed order). *)
 val focus_context : focus_context -> Evar.t list * Evar.t list
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 80eb9d0124..8ed75a8d00 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -252,7 +252,7 @@ module Giveup : Writer with type t = goal list = struct
   let put gs = Logical.put (true, gs)
 end
 
-(** Lens and utilies pertaining to the info trace *)
+(** Lens and utilities pertaining to the info trace *)
 module InfoL = struct
   let recording = Logical.(map (fun {P.trace} -> trace) current)
   let if_recording t =
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 3437b6ce77..f0c9fdb589 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -145,7 +145,7 @@ module Shelf : State with type t = goal list
     of the tactic. *)
 module Giveup : Writer with type t = goal list
 
-(** Lens and utilies pertaining to the info trace *)
+(** Lens and utilities pertaining to the info trace *)
 module InfoL : sig
   (** [record_trace t] behaves like [t] and compute its [info] trace. *)
   val record_trace : 'a Logical.t -> 'a Logical.t
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index fcbf305f9d..4f9f9ce6a5 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -353,7 +353,7 @@ let normalize_context_set g ctx us algs weak =
       noneqs Constraint.empty
   in
   (* Compute the left and right set of flexible variables, constraints
-     mentionning other variables remain in noneqs. *)
+     mentioning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr =
     Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
       let lus = LMap.mem l us and rus = LMap.mem r us in
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index 1069d0bfa3..2e7dfc42db 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -173,7 +173,7 @@ type strexpr =
 
 (** {5 Dynamic semantics} *)
 
-(** Values are represented in a way similar to OCaml, i.e. they constrast
+(** Values are represented in a way similar to OCaml, i.e. they contrast
     immediate integers (integers, constructors without arguments) and structured
     blocks (tuples, arrays, constructors with arguments), as well as a few other
     base cases, namely closures, strings, named constructors, and dynamic type
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index d646b5cda5..829570a354 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -20,7 +20,7 @@ val is_value : glb_tacexpr -> bool
 val check_unit : ?loc:Loc.t -> type_scheme -> unit
 
 val check_subtype : type_scheme -> type_scheme -> bool
-(** [check_subtype t1 t2] returns [true] iff all values of intances of type [t1]
+(** [check_subtype t1 t2] returns [true] iff all values of instances of type [t1]
     also have type [t2]. *)
 
 val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr
diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml
index 058d02adde..354a578cb3 100644
--- a/user-contrib/Ltac2/tac2match.ml
+++ b/user-contrib/Ltac2/tac2match.ml
@@ -88,7 +88,7 @@ module PatternMatching (E:StaticEnvironment) = struct
 
   (** To focus on the algorithmic portion of pattern-matching, the
       bookkeeping is relegated to a monad: the composition of the
-      bactracking monad of {!IStream.t} with a "writer" effect. *)
+      backtracking monad of {!IStream.t} with a "writer" effect. *)
   (* spiwack: as we don't benefit from the various stream optimisations
      of Haskell, it may be costly to give the monad in direct style such as
      here. We may want to use some continuation passing style. *)