Fixing typos - Part 1

11 files changed, 19 insertions, 19 deletions

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