Fixing typos - Part 2

4 files changed, 20 insertions, 20 deletions

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