Backport PR #10203: Fixing typos - Part 1

.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>

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

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).

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 ...
 
 #########################

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}/' $< > $@

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

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

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).
  *)

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. *)

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"

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. *)

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^>

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 ====================

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

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"

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

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.

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

dev/doc/archive/naming-conventions.tex

@@ -570,11 +570,11 @@ \section{Arithmetical conventions}
 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])\\

dev/doc/archive/versions-history.tex

@@ -372,7 +372,7 @@
 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]\\

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 :

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 run even if option -n is given to make
+a command starting by @ is not echoed before being run
 
 * 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)
 ------------------------

dev/doc/changes.md

@@ -1271,7 +1271,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
@@ -1586,7 +1586,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.

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`.
 

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

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

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

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*.
 
 -------------------------------
 

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

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 :
 ;