24 files changed, 46 insertions, 56 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index c2ca6ebaa4..46f8572b94 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -212,6 +212,9 @@ windows32:
   <<: *windows-template
   variables:
     ARCH: "32"
+  except:
+    - /^pr-.*$/
+
 
 pkg:nix:
   image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index aee4dd74d8..521dfe2a3f 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -793,7 +793,7 @@ function make_ln {
 
 function make_ocaml {
   get_flex_dll_link_bin
-  if build_prep https://github.com/ocaml/ocaml/archive/4.07.0 ocaml-4.07.0 tar.gz 1 ; then
+  if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then
     # See README.win32.adoc
     cp config/m-nt.h byterun/caml/m.h
     cp config/s-nt.h byterun/caml/s.h
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 43d680af61..a814e4914e 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -138,14 +138,11 @@ persists to and is used by the next jobs.
 
 Artifacts can also be downloaded from the GitLab repository.
 Currently, available artifacts are:
-- the Coq executables and stdlib, in three copies varying in
+- the Coq executables and stdlib, in four copies varying in
   architecture and OCaml version used to build Coq.
-- the Coq documentation, built only in the `build:base` job. When submitting
+- the Coq documentation, built in the `documentation` job. When submitting
   a documentation PR, this can help reviewers checking the rendered result.
 
-As an exception to the above, jobs testing that compilation triggers
-no OCaml warnings build Coq in parallel with other tests.
-
 ### GitLab and Windows
 
 If your repository has access to runners tagged `windows`, setting the
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 1643baf0e8..2264b170fc 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -303,7 +303,7 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
        it names the introduced hypothesis :token:`ident`.
 
     Note that this example also uses ``:token:``.  That's because ``ident`` is
-    defined in the the Coq manual as a grammar production, and ``:token:``
+    defined in the Coq manual as a grammar production, and ``:token:``
     creates a link to that.  When referring to a placeholder that happens to be
     a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
 
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 0f51b3eba3..88da58c27d 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -107,7 +107,7 @@ and ``coqtop``, unless stated otherwise:
   to the OCaml loadpath. See also: :ref:`names-of-libraries` and the
   command Declare ML Module Section :ref:`compiled-files`.
 :-Q *directory* dirpath: Add physical path *directory* to the list of
-  directories where |Coq| looks for a file and bind it to the the logical
+  directories where |Coq| looks for a file and bind it to the logical
   directory *dirpath*. The subdirectory structure of *directory* is
   recursively available from |Coq| using absolute names (extending the
   dirpath prefix) (see Section :ref:`qualified-names`).Note that only those
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 6fbb2fac6d..0310dbead5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -391,7 +391,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    focused goal independently and stops if it succeeds; otherwise it
    tries to apply :n:`v__2` and so on. It fails when there is no
    applicable tactic. In other words,
-   :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first
+   :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the first
    :n:`v__i` to have *at least* one success.
 
    .. exn:: No applicable tactic.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index a9d0c16376..e9aacba3a5 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -358,8 +358,10 @@ same bullet ``b``. See the example below.
 
 Different bullets can be used to nest levels. The scope of bullet does
 not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
-nesting levels provided they are delimited by these. Available bullets
-are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period).
+nesting levels provided they are delimited by these. Bullets are made of
+repeated ``-``, ``+`` or ``*`` symbols:
+
+.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * }
 
 Note again that when a focused goal is proved a message is displayed
 together with a suggestion about the right bullet or ``}`` to unfocus it
@@ -392,19 +394,23 @@ The following example script illustrates all these features:
     - assert True.
     { trivial. }
     assumption.
+    Qed.
 
+.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished.
 
-.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished.
-
-   Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same.
+   Before using bullet :n:`@bullet__1` again, you should first finish proving
+   the current focused goal.
+   Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same.
 
-.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here.
+.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here.
 
-   You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here.
+   You must put :n:`@bullet__2` to focus on the next goal. No other bullet is
+   allowed here.
 
 .. exn:: No such goal. Focus next goal with bullet @bullet.
 
-   You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is  mandatory here.
+   You tried to apply a tactic but no goals were under focus.
+   Using :n:`@bullet` is  mandatory here.
 
 .. exn:: No such goal. Try unfocusing with %{.
 
@@ -433,7 +439,7 @@ Requesting information
 
    .. cmdv:: Show @num
 
-      Displays only the :token:`num` th subgoal.
+      Displays only the :token:`num`\-th subgoal.
 
       .. exn:: No such goal.
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index e6b71a8293..a0dc16aac7 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -449,7 +449,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
        it names the introduced hypothesis :token:`ident`.
 
     Note that this example also uses ``:token:``.  That's because ``ident`` is
-    defined in the the Coq manual as a grammar production, and ``:token:``
+    defined in the Coq manual as a grammar production, and ``:token:``
     creates a link to that.  When referring to a placeholder that happens to be
     a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
     """
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 439274240f..ad11f853ca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -351,7 +351,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
 	      Locusops.onConcl);
 	    observe_tac ("toto ") tclIDTAC;
     
-	    (* introducing the the result of the graph and the equality hypothesis *)
+            (* introducing the result of the graph and the equality hypothesis *)
 	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 7143f51853..d5d36c97fa 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -41,7 +41,7 @@ val register_alias : alias -> alias_tactic -> unit
 (** Register a tactic alias. *)
 
 val interp_alias : alias -> alias_tactic
-(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+(** Recover the body of an alias. Raises an anomaly if it does not exist. *)
 
 val check_alias : alias -> bool
 (** Returns [true] if an alias is defined, false otherwise. *)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 54f3f9c718..1f3c758e5c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -469,7 +469,7 @@ let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
 (* term mkApp (t', args) is convertible to t.                        *)
 (* This makes a useful shorthand for local definitions in proofs,    *)
 (* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *)
-(* and, in context of the the 4CT library, pose mid := maps id means *)
+(* and, in context of the 4CT library, pose mid := maps id means *)
 (*    pose mid := fun d : detaSet => @maps d d (@id (datum d))       *)
 (* Note that this facility does not extend to set, which tries       *)
 (* instead to fill holes by matching a goal subterm.                 *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b379cdf410..ec0ff73062 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -633,7 +633,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
           dependency status (of course, Anonymous implies non
           dependent, but not conversely).
 
-          From Coq > 8.2, using or not the the effective dependency of
+          From Coq > 8.2, using or not the effective dependency of
           the predicate is parametrable! *)
 
           begin match na with
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
deleted file mode 100644
index 37ec6dacca..0000000000
--- a/stm/workerLoop.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Default priority *)
-val async_proofs_worker_priority : CoqworkmgrApi.priority ref
-
-val loop :
-  (unit -> unit) -> Coqargs.coq_cmdopts -> string list ->
-    Coqargs.coq_cmdopts * string list
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 3c9b6b428b..dcaea894eb 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -15,7 +15,7 @@
     It follows the implementation from Ocaml's standard library,
 
     All operations given here expect and produce well-balanced trees
-    (in the ocaml sense: heigths of subtrees shouldn't differ by more
+    (in the ocaml sense: heights of subtrees shouldn't differ by more
     than 2), and hence has low complexities (e.g. add is logarithmic
     in the size of the set). But proving these balancing preservations
     is in fact not necessary for ensuring correct operational behavior
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 56844f4773..59b2f789ab 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
 auto with set.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma union_subset_1: subset s (union s s')=true.
 Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
 rewrite not_mem_iff; auto.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma inter_subset_1: subset (inter s s') s=true.
 Proof.
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 1ee098cb07..4f2fdcf94c 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
 auto with set.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma union_subset_1: subset s (union s s')=true.
 Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
 rewrite not_mem_iff; auto.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma inter_subset_1: subset (inter s s') s=true.
 Proof.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 9d2a73ed0f..95868861fa 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -13,7 +13,7 @@
     This module factorizes common parts in implementations
     of finite sets as AVL trees and as Red-Black trees. The nodes
     of the trees defined here include an generic information
-    parameter, that will be the heigth in AVL trees and the color
+    parameter, that will be the height in AVL trees and the color
     in Red-Black trees. Without more details here about these
     information parameters, trees here are not known to be
     well-balanced, but simply binary-search-trees.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 2da4452819..4aabda77ee 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -80,7 +80,7 @@ Proof.
  now apply testbit_even_succ.
 Qed.
 
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
 
 (** This concise equation could have been taken as specification
    for testbit in the interface, but it would have been hard to
@@ -102,10 +102,10 @@ Proof.
  left. destruct b; split; simpl; order'.
 Qed.
 
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
    power was initially taken as specification for testbit.
    We describe [a] as having a low part and a high part, with
-   the corresponding bit in the middle. This caracterisation
+   the corresponding bit in the middle. This characterisation
    is moderatly complex to implement, but also moderately
    usable... *)
 
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index e1391f5990..90663de3f2 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -78,7 +78,7 @@ Proof.
  apply testbit_even_succ, le_0_l.
 Qed.
 
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
 
 (** This concise equation could have been taken as specification
    for testbit in the interface, but it would have been hard to
@@ -99,10 +99,10 @@ Proof.
  destruct b; order'.
 Qed.
 
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
    power was initially taken as specification for testbit.
    We describe [a] as having a low part and a high part, with
-   the corresponding bit in the middle. This caracterisation
+   the corresponding bit in the middle. This characterisation
    is moderatly complex to implement, but also moderately
    usable... *)
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 6a3dd97656..9b8dd1db0b 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -392,7 +392,7 @@ Definition cond_positivity (x:R) : bool :=
     | right _ => false
   end.
 
-(** Sequential caracterisation of continuity *)
+(** Sequential characterisation of continuity *)
 Lemma continuity_seq :
   forall (f:R -> R) (Un:nat -> R) (l:R),
     continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 05edc6ccde..4d04667c01 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -83,7 +83,7 @@ End GenericMinMax.
 Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
  Module Import Private_Tac := !MakeOrderTac O O.
 
-(** An alternative caracterisation of [max], equivalent to
+(** An alternative characterisation of [max], equivalent to
     [max_l /\ max_r] *)
 
 Lemma max_spec n m :
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 900964609d..113ba3684c 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -425,7 +425,7 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-worker-id" -> set_worker_id opt (next ()); oval
 
     |"-compat" ->
-      let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in
+      let v = G_vernac.parse_compat_version (next ()) in
       Flags.compat_version := v;
       add_compat_require oval v
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ee578669c2..e33aa38173 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let destruct_ind sigma c =
   then avoid should be
  [| lb_An ... lb _A1  (resp. bl_An ... bl_A1)
     eq_An .... eq_A1 An ... A1 |]
-so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
+so from Ai we can find the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
 let do_replace_lb mode lb_scheme_key aavoid narg p q =
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index b959f2afa9..74516e320c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -59,7 +59,7 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-let parse_compat_version ?(allow_old = true) = let open Flags in function
+let parse_compat_version = let open Flags in function
   | "8.8" -> Current
   | "8.7" -> V8_7
   | "8.6" -> V8_6