20 files changed, 38 insertions, 38 deletions
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}