Fixing typos - Part 2

30 files changed, 60 insertions, 60 deletions

diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index 4bc3dba36e..bc7e1448f7 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -200,7 +200,7 @@ For the moment there are:
 	Wf.well_founded_induction
 	Wf.well_founded_induction_type
 Those constants does not match the auto-inlining criterion based on strictness.
-Of course, you can still overide this behaviour via some Extraction NoInline. 
+Of course, you can still override this behaviour via some Extraction NoInline. 
 
 * There is now a web page showing the extraction of all standard theories: 
 http://www.lri.fr/~letouzey/extraction
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 36bb1148b6..02da168fd0 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ].
 Extract Inductive sumbool => bool [ true false ].
 Extract Inductive sumor => option [ Some None ].
 
-(** Restore lazyness of andb, orb.
+(** Restore laziness of andb, orb.
     NB: without these Extract Constant, andb/orb would be inlined
-    by extraction in order to have lazyness, producing inelegant
+    by extraction in order to have laziness, producing inelegant
     (if ... then ... else false) and (if ... then true else ...).
 *)
 
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 59c57cc544..f46d09e335 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -573,7 +573,7 @@ let pp_ocaml_gen k mp rls olab =
 	if is_mp_bound base then pp_ocaml_bound base rls
 	else pp_ocaml_extern k base rls
 
-(* For Haskell, things are simplier: we have removed (almost) all structures *)
+(* For Haskell, things are simpler: we have removed (almost) all structures *)
 
 let pp_haskell_gen k mp rls = match rls with
   | [] -> assert false
@@ -590,7 +590,7 @@ let pp_global k r =
   let s = List.hd ls in
   let mp,l = repr_of_r r in
   if ModPath.equal mp (top_visible_mp ()) then
-    (* simpliest situation: definition of r (or use in the same context) *)
+    (* simplest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
     (add_visible (k,s) l; unquote s)
   else
@@ -607,7 +607,7 @@ let pp_module mp =
   let ls = mp_renaming mp in
   match mp with
     | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) ->
-	(* simpliest situation: definition of mp (or use in the same context) *)
+        (* simplest situation: definition of mp (or use in the same context) *)
 	(* we update the visible environment *)
 	let s = List.hd ls in
 	add_visible (Mod,s) l; s
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index d7bb27f121..db1a389fe7 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
-(* Same, with content splitted in several files *)
+(* Same, with content split in several files *)
 | [ "Separate" "Extraction" ne_global_list(l) ]
   -> { separate_extraction l }
 END
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 4e229a94b6..c2c48f9565 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -101,7 +101,7 @@ let labels_of_ref r =
 
 (*S The main tables: constants, inductives, records, ... *)
 
-(* Theses tables are not registered within coq save/undo mechanism
+(* These tables are not registered within coq save/undo mechanism
    since we reset their contents at each run of Extraction *)
 
 (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum
@@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj =
     ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)))
 
 let in_custom_matchs : GlobRef.t * string -> obj =
-  declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs"
+  declare_object @@ superglobal_object_nodischarge "ML extractions custom matches"
     ~cache:(fun (_,(r,s)) -> add_custom_match r s)
     ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s)))
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 287a374ab1..cffe8a3e78 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -658,7 +658,7 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 
 	*)
 	(fun g ->
-(* 	   observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
+(* 	   observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
 	   thin [hid] g
 	)
       )
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e9a2c285d0..f51c6dc6be 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -429,11 +429,11 @@ let get_funs_constant mp =
     let l_const = get_funs_constant const f in
     (*
        We need to check that all the functions found are in the same block
-       to prevent Reset stange thing
+       to prevent Reset strange thing
     *)
     let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
     let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in
-    (* all the paremeter must be equal*)
+    (* all the parameters must be equal*)
     let _check_params =
       let first_params = List.hd l_params  in
       List.iter
@@ -514,7 +514,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
       )
       fas
   in
-  (* We create the first priciple by tactic *)
+  (* We create the first principle by tactic *)
   let first_type,other_princ_types =
     match l_schemes with
 	s::l_schemes -> s,l_schemes
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e15e167ff3..4c67d65816 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1369,7 +1369,7 @@ let do_build_inductive
 	(rebuild_return_type returned_types.(i))
     in
     (* We need to lift back our work topconstr but only with all information
-       We mimick a Set Printing All.
+       We mimic a Set Printing All.
        Then save the graphs and reset Printing options to their primitive values
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
@@ -1438,7 +1438,7 @@ let do_build_inductive
       (rebuild_return_type returned_types.(i))
   in
   (* We need to lift back our work topconstr but only with all information
-     We mimick a Set Printing All.
+     We mimic a Set Printing All.
      Then save the graphs and reset Printing options to their primitive values
   *)
   let rel_arities = Array.mapi rel_arity funsargs in
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 481a8be3ba..24b3690138 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -55,7 +55,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
     Glob_term.cases_pattern * Id.Map.key list *
       Id.t Id.Map.t
 
-(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
+(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result respects barendregt
    conventions and  does not share bound variables with avoid
 *)
 val alpha_rt : Id.t list -> glob_constr -> glob_constr
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 40f66ce5eb..48cf040919 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -115,7 +115,7 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq"))
 let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 
 (*****************************************************************)
-(* Copy of the standart save mechanism but without the much too  *)
+(* Copy of the standard save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
 open Entries
@@ -357,7 +357,7 @@ let add_Function is_general f =
 
 let pr_table env sigma = pr_table env sigma !from_function
 (*********************************)
-(* Debuging *)
+(* Debugging *)
 let functional_induction_rewrite_dependent_proofs = ref true
 let function_debug = ref false
 open Goptions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index edb698280f..2a0140f02c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -591,7 +591,7 @@ let rec reflexivity_with_destruct_cases g =
 
 
 (* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
-   is the tactic used to prove completness lemma.
+   is the tactic used to prove completeness lemma.
 
    [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions
    (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct.
@@ -748,7 +748,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let map (c, u) = mkConstU (c, EInstance.make u) in
   let funs_constr = Array.map map funs  in
-  (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+  (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify
     (fun () ->
      let env = Global.env () in
@@ -928,7 +928,7 @@ let revert_graph kn post_tac hid g =
    [hid] is the hypothesis to invert, [fconst] is the function to invert and  [f_correct]
    is the correctness lemma for [fconst].
 
-   The sketch is the follwing~:
+   The sketch is the following~:
    \begin{enumerate}
    \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$
    (fails if it is not possible)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1fca132655..216be3797b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1584,7 +1584,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 			   spc () ++ str"is defined" )
       )
   in
-  (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+  (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify (fun () ->
       let pstate = com_terminate
           tcc_lemma_name
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 963b7189f9..f772da69a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -207,7 +207,7 @@ end) = struct
   let mk_relation env evd a = 
     app_poly env evd relation [| a |]
 
-  (** Build an infered signature from constraints on the arguments and expected output
+  (** Build an inferred signature from constraints on the arguments and expected output
       relation *)
     
   let build_signature evars env m (cstrs : (types * types option) option list)
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 0eb7726a18..8bd69dd4fd 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
   | Select  (* returns all successes of the first matching branch *)
-  | Once    (* returns the first success in a maching branch
+  | Once    (* returns the first success in a matching branch
                (not necessarily the first) *)
 type global_flag = (* [gfail] or [fail] *)
   | TacGlobal
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index fd303f5d94..f839c3e886 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
   | Select  (* returns all successes of the first matching branch *)
-  | Once    (* returns the first success in a maching branch
+  | Once    (* returns the first success in a matching branch
                (not necessarily the first) *)
 type global_flag = (* [gfail] or [fail] *)
   | TacGlobal
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 800be2565d..4a0b01bcdc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function
   | NamedHyp id ->
       (* If a name is bound, it has to be a quantified hypothesis *)
       (* user has to use other names for variables if these ones clash with *)
-      (* a name intented to be used as a (non-variable) identifier *)
+      (* a name intended to be used as a (non-variable) identifier *)
       try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
@@ -2075,7 +2075,7 @@ let _ =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun; poly; extra; } in
     let tac = interp_tactic ist tac in
-    (* EJGA: We sould also pass the proof name if desired, for now
+    (* EJGA: We should also pass the proof name if desired, for now
        poly seems like enough to get reasonable behavior in practice
      *)
     let name, poly = Id.of_string "ltac_gen", poly in
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 2b5e496168..7783661787 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -128,7 +128,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. *)
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index e0e2232be5..7759bda7c7 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -129,7 +129,7 @@ Proof.
 intros n m H1 H2; rewrite H2 in H1; now apply H1.
 Qed.
 
-(* Propeties of plus, minus and opp *)
+(* Properties of plus, minus and opp *)
 
 Theorem Rplus_0_l : forall n : R, 0 + n == n.
 Proof.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 60931df517..c5e179fbb8 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -990,7 +990,7 @@ Proof.
   rewrite IHs. reflexivity.
 Qed.
 
-(** equality migth be (too) strong *)
+(** equality might be (too) strong *)
 Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f).
 Proof.
   destruct f.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index bed9e55ac0..48027442b2 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1208,8 +1208,8 @@ let dump_rexpr = lazy
     
     
 (** [make_goal_of_formula depxr vars props form] where 
-     - vars is an environment for the arithmetic variables occuring in form
-     - props is an environment for the propositions occuring in form
+     - vars is an environment for the arithmetic variables occurring in form
+     - props is an environment for the propositions occurring in form
     @return a goal where all the variables and propositions of the formula are quantified
 
 *) 
@@ -1469,7 +1469,7 @@ let pre_processZ mt f =
    x <= y or (x and y are incomparable) *)
 
 (**
-  * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
+  * Instantiate the current Coq goal with a Micromega formula, a varmap, and a
   * witness.
   *)
 
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 0209030b64..f038f8a71a 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -21,7 +21,7 @@ module type PHashtable =
 
     val open_in : string -> 'a t
     (** [open_in f] rebuilds a table from the records stored in file [f].
-	As marshaling is not type-safe, it migth segault.
+        As marshaling is not type-safe, it might segfault.
     *)
 
     val find : 'a t -> key -> 'a
diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli
index 4e7a388aaf..d2f3e756a9 100644
--- a/plugins/micromega/persistent_cache.mli
+++ b/plugins/micromega/persistent_cache.mli
@@ -17,7 +17,7 @@ module type PHashtable =
 
     val open_in : string -> 'a t
     (** [open_in f] rebuilds a table from the records stored in file [f].
-        As marshaling is not type-safe, it migth segault.
+        As marshaling is not type-safe, it might segfault.
     *)
 
     val find : 'a t -> key -> 'a
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index 6aebc4ca9a..e3a9f6f60f 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -200,7 +200,7 @@ let is_undefined f =
   | _ -> false;;
 
 (* ------------------------------------------------------------------------- *)
-(* Operation analagous to "map" for lists.                                   *)
+(* Operation analogous to "map" for lists.                                   *)
 (* ------------------------------------------------------------------------- *)
 
 let mapf =
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 1777418ef6..bece316c7d 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -267,7 +267,7 @@ module PIdeal = Ideal.Make(Poly)
 open PIdeal
 
 (* term to sparse polynomial 
-   varaibles <=np are in the coefficients
+   variables <=np are in the coefficients
 *)
 
 let term_pol_sparse nvars np t=
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 5db587b9cc..f6ca232c2e 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -357,7 +357,7 @@ let remP v p =
   moinsP p (multP (coefDom v p) (puisP (x v) (deg v p)))
 
 
-(* first interger coefficient of p *)
+(* first integer coefficient of p *)
 let rec coef_int_tete p =
   let v = max_var_pol p in
     if v>0
@@ -526,7 +526,7 @@ let div_pol_rat p q=
 
 (* pseudo division :
    q = c*x^m+q1
-   retruns (r,c,d,s) s.t. c^d*p = s*q + r.
+   returns (r,c,d,s) s.t. c^d*p = s*q + r.
 *)
 
 let pseudo_div p q x =
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 49d729bd6c..c5f387b248 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -49,7 +49,7 @@ Require Import ssreflect ssrfun.
                             altP (idP my_formula) but circumventing the
                             dependent index capture issue; destructing
                             boolP my_formula generates two subgoals with
-                            assumtions my_formula and ~~ myformula. As
+                            assumptions my_formula and ~~ myformula. As
                             with altP, my_formula must be an application.
             \unless C, P <-> we can assume property P when a something that
                             holds under condition C (such as C itself).
@@ -64,7 +64,7 @@ Require Import ssreflect ssrfun.
                          := forall b : bool, (P -> b) -> b.
                             This is equivalent to ~ (~ P) when P : Prop.
              implies P Q == wrapper variant type that coerces to P -> Q and
-                            can be used as a P -> Q view unambigously.
+                            can be used as a P -> Q view unambiguously.
                             Useful to avoid spurious insertion of <-> views
                             when Q is a conjunction of foralls, as in Lemma
                             all_and2 below; conversely, avoids confusion in
@@ -1003,7 +1003,7 @@ Proof. by case: a; case: b. Qed.
 Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b.
 Proof. by case: a; case: b. Qed.
 
-(**  Pseudo-cancellation -- i.e, absorbtion  **)
+(**  Pseudo-cancellation -- i.e, absorption  **)
 
 Lemma andbK a b : a && b || a = a.  Proof. by case: a; case: b. Qed.
 Lemma andKb a b : a || b && a = a.  Proof. by case: a; case: b. Qed.
@@ -1245,7 +1245,7 @@ Notation "[ 'pred' x : T | E1 & E2 ]" :=
 (** Coercions for simpl_pred.
    As simpl_pred T values are used both applicatively and collectively we
  need simpl_pred to coerce to both pred T _and_ {pred T}. However it is
- undesireable to have two distinct constants for what are essentially identical
+ undesirable to have two distinct constants for what are essentially identical
  coercion functions, as this confuses the SSReflect keyed matching algorithm.
  While the Coq Coercion declarations appear to disallow such Coercion aliasing,
  it is possible to work around this limitation with a combination of modules
@@ -1331,9 +1331,9 @@ Variant mem_pred T := Mem of pred T.
   Similarly to pred_of_simpl, it will usually not be inserted by type
   inference, as all mem_pred mp =~= pred_sort ?pT unification problems will
   be solve by the memPredType instance below; pred_of_mem will however
-  be used if a mem_pred T is used as a {pred T}, which is desireable as it
+  be used if a mem_pred T is used as a {pred T}, which is desirable as it
   will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma
-  expection a generic collective predicate p : {pred T} and premise x \in P
+  exception a generic collective predicate p : {pred T} and premise x \in P
   will display a subgoal x \in A rathere than x \in mem A.
     Conversely, pred_of_mem will _not_ if it is used id (mem A) is used
   applicatively or as a pred T; there the simpl_of_mem coercion defined below
@@ -1396,7 +1396,7 @@ Notation "[ 'rel' x y 'in' A & B ]" :=
 Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope.
 Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope.
 
-(** Aliases of pred T that let us tag intances of simpl_pred as applicative
+(** Aliases of pred T that let us tag instances of simpl_pred as applicative
   or collective, via bespoke coercions. This tagging will give control over
   the simplification behaviour of inE and othe rewriting lemmas below.
     For this control to work it is crucial that collective_of_simpl _not_
@@ -1428,7 +1428,7 @@ Implicit Types (mp : mem_pred T).
   - registered_applicative_pred: this user-facing structure is used to
     declare values of type pred T meant to be used applicatively. The
     structure parameter merely displays this same value, and is used to avoid
-    undesireable, visible occurrence of the structure in the right hand side
+    undesirable, visible occurrence of the structure in the right hand side
     of rewrite rules such as app_predE.
       There is a canonical instance of registered_applicative_pred for values
     of the applicative_of_simpl coercion, which handles the
@@ -1454,7 +1454,7 @@ Implicit Types (mp : mem_pred T).
     has been fixed earlier by the manifest_mem_pred match. In particular the
     definition of a predicate using the applicative_pred_of_simpl idiom above
     will not be expanded - this very case is the reason in_applicative uses
-    a mem_pred telescope in its left hand side. The more straighforward
+    a mem_pred telescope in its left hand side. The more straightforward
     ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap))
     with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...]
     rather than ?p := Apred in the example above.
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 5e3e8ce5fb..572d72ccd8 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -132,7 +132,7 @@ Delimit Scope ssripat_scope with ssripat.
  Make the general "if" into a notation, so that we can override it below.
  The notations are "only parsing" because the Coq decompiler will not
  recognize the expansion of the boolean if; using the default printer
- avoids a spurrious trailing %%GEN_IF. **)
+ avoids a spurious trailing %%GEN_IF. **)
 
 Declare Scope general_if_scope.
 Delimit Scope general_if_scope with GEN_IF.
@@ -347,10 +347,10 @@ Register protect_term as plugins.ssreflect.protect_term.
 
 (**
  The ssreflect idiom for a non-keyed pattern:
-  - unkeyed t wiil match any subterm that unifies with t, regardless of
+  - unkeyed t will match any subterm that unifies with t, regardless of
     whether it displays the same head symbol as t.
   - unkeyed t a b will match any application of a term f unifying with t,
-    to two arguments unifying with with a and b, repectively, regardless of
+    to two arguments unifying with with a and b, respectively, regardless of
     apparent head symbols.
   - unkeyed x where x is a variable will match any subterm with the same
     type as x (when x would raise the 'indeterminate pattern' error).        **)
@@ -380,7 +380,7 @@ Notation "=^~ r" := (ssr_converse r) : form_scope.
   locked_with k t is equal but not convertible to t, much like locked t,
     but supports explicit tagging with a value k : unit. This is used to
     mitigate a flaw in the term comparison heuristic of the Coq kernel,
-    which treats all terms of the form locked t as equal and conpares their
+    which treats all terms of the form locked t as equal and compares their
     arguments recursively, leading to an exponential blowup of comparison.
     For this reason locked_with should be used rather than locked when
     defining ADT operations. The unlock tactic does not support locked_with
@@ -523,7 +523,7 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
    elim/abstract_context: (pattern) => G defG.
    vm_compute; rewrite {}defG {G}.
  Note that vm_cast are not stored in the proof term
- for reductions occuring in the context, hence
+ for reductions occurring in the context, hence
    set here := pattern; vm_compute in (value of here)
  blows up at Qed time.                                        **)
 Lemma abstract_context T (P : T -> Type) x :
@@ -637,7 +637,7 @@ Ltac over :=
     later complain that it cannot erase _top_assumption_ after having
     abstracted the viewed assumption. Making x and y maximal implicits
     would avoid this and force the intended @Some_inj nat x y _top_assumption_
-    interpretation, but is undesireable as it makes it harder to use Some_inj
+    interpretation, but is undesirable as it makes it harder to use Some_inj
     with the many SSReflect and MathComp lemmas that have an injectivity
     premise. Specifying {T : nonPropType} solves this more elegantly, as then
     (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop.
@@ -655,13 +655,13 @@ Module NonPropType.
     maybeProp T to tt and use the test_negative instance and set ?r to false.
   - call_of c r sets up a call to test_of on condition c with expected result r.
     It has a default instance for its 'callee' projection to Type, which
-    sets c := maybeProj T and r := false whe unifying with a type T.
+    sets c := maybeProj T and r := false when unifying with a type T.
   - type is a telescope on call_of c r, which checks that unifying test_of ?r1
     with c indeed sets ?r1 := r; the type structure bundles the 'test' instance
     and its 'result' value along with its call_of c r projection. The default
     instance essentially provides eta-expansion for 'type'. This is only
     essential for the first 'result' projection to bool; using the instance
-    for other projection merely avoids spurrious delta expansions that would
+    for other projection merely avoids spurious delta expansions that would
     spoil the notProp T notation.
  In detail, unifying T =~= ?S with ?S : nonPropType, i.e.,
   (1)  T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S)
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 675e4d2457..dbc9bb24c5 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -96,7 +96,7 @@ let subgoals_tys sigma (relctx, concl) =
  *    (occ, c), deps and the pattern inferred from the type of the eliminator
  * 3. build the new predicate matching the patterns, and the tactic to 
  *    generalize the equality in case eqid is not None
- * 4. build the tactic handle intructions and clears as required in ipats and
+ * 4. build the tactic handle instructions and clears as required in ipats and
  *    by eqid *)
 
 let get_eq_type gl =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 93c0d5c236..59fc69f100 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -128,7 +128,7 @@ let newssrcongrtac arg ist gl =
     x, re_sig si sigma in
   let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
   let ssr_congr lr = EConstr.mkApp (arr, lr) in
-  (* here thw two cases: simple equality or arrow *)
+  (* here the two cases: simple equality or arrow *)
   let equality, _, eq_args, gl' =
     let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
     pf_saturate gl (EConstr.of_constr eq) 3 in
@@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i
 (* Coq has a more general form of "equation" (any type with a single *)
 (* constructor with no arguments with_rect_r elimination lemmas).    *)
 (* However there is no clear way of determining the LHS and RHS of   *)
-(* such a generic Leibnitz equation -- short of inspecting the type  *)
+(* such a generic Leibniz equation -- short of inspecting the type  *)
 (* of the elimination lemmas.                                        *)
 
 let rec strip_prod_assum c = match Constr.kind c with
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 25975c84e8..6d1d858648 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -143,7 +143,7 @@ val mk_tpattern :
 type find_P =
   env -> constr -> int -> k:subst -> constr
 
-(** [conclude ()] asserts that all mentioned ocurrences have been visited.
+(** [conclude ()] asserts that all mentioned occurrences have been visited.
   @return the instance of the pattern, the evarmap after the pattern
     instantiation, the proof term and the ssrdit stored in the tpattern
   @raise UserEerror if too many occurrences were specified *)