Fixing typos - Part 3

18 files changed, 22 insertions, 22 deletions

diff --git a/test-suite/bugs/closed/bug_2137.v b/test-suite/bugs/closed/bug_2137.v
index b1f54b1766..981cc94dc1 100644
--- a/test-suite/bugs/closed/bug_2137.v
+++ b/test-suite/bugs/closed/bug_2137.v
@@ -3,7 +3,7 @@
 The fsetdec tactic is sensitive to which way round the arguments to <> are.
 In the small, self-contained example below, it is able to solve the goal
 if it knows that "b <> a", but not if it knows that "a <> b". I would expect
-it to be able to solve hte goal in either case.
+it to be able to solve the goal in either case.
 
 I have coq r12238.
 
diff --git a/test-suite/bugs/closed/bug_2603.v b/test-suite/bugs/closed/bug_2603.v
index 371bfdc575..64c656a7a6 100644
--- a/test-suite/bugs/closed/bug_2603.v
+++ b/test-suite/bugs/closed/bug_2603.v
@@ -3,7 +3,7 @@
 As noticed by A. Appel in bug #2603, module names and definition
 names used to be in the same namespace. But conflict with names
 of constructors (or 2nd mutual inductive...) used to not be checked
-enough, leading to stange situations.
+enough, leading to strange situations.
 
 - In 8.3pl3 we introduced checks that forbid uniformly the following
   situations.
diff --git a/test-suite/bugs/closed/bug_3080.v b/test-suite/bugs/closed/bug_3080.v
index 36ab7ff599..06719653fe 100644
--- a/test-suite/bugs/closed/bug_3080.v
+++ b/test-suite/bugs/closed/bug_3080.v
@@ -15,4 +15,4 @@ Notation " g ∘ f " := (compose g f)
   (at level 40, left associativity) : function_scope.
 
 Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *)
-Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *)
+Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arguments to [compose] *)
diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v
index 5162f352df..26731e3292 100644
--- a/test-suite/bugs/closed/bug_4503.v
+++ b/test-suite/bugs/closed/bug_4503.v
@@ -29,7 +29,7 @@ End ILogic.
 
 Set Printing Universes.
 
-(* There is stil a problem if the class is universe polymorphic *)
+(* There is still a problem if the class is universe polymorphic *)
 Section Embed_ILogic_Pre.
   Polymorphic Universes A T.
   Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
diff --git a/test-suite/bugs/closed/bug_4720.v b/test-suite/bugs/closed/bug_4720.v
index 704331e784..a870792c39 100644
--- a/test-suite/bugs/closed/bug_4720.v
+++ b/test-suite/bugs/closed/bug_4720.v
@@ -34,7 +34,7 @@ End WithModPriv.
    identical by the extraction.
 
    In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv
-   were all causing Anomaly or Assert Failure. This shoud be fixed now.
+   were all causing Anomaly or Assert Failure. This should be fixed now.
 *)
 
 Require Extraction.
diff --git a/test-suite/bugs/closed/bug_5123.v b/test-suite/bugs/closed/bug_5123.v
index 17231bffcf..a4029aeee0 100644
--- a/test-suite/bugs/closed/bug_5123.v
+++ b/test-suite/bugs/closed/bug_5123.v
@@ -28,6 +28,6 @@ Goal True.
   opose (@vect_sigT_eqdec _ _ _ _) as H.
   Unshelve.
   all:cycle 3.
-  eapply existT. (*This does no typeclass resultion, which is correct.*)
+  eapply existT. (*This does no typeclass resolution, which is correct.*)
   Focus 5.
 Abort.
diff --git a/test-suite/bugs/closed/bug_5149.v b/test-suite/bugs/closed/bug_5149.v
index ae32217057..b56abfe42e 100644
--- a/test-suite/bugs/closed/bug_5149.v
+++ b/test-suite/bugs/closed/bug_5149.v
@@ -36,7 +36,7 @@ Proof.
   solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail
 "too early".
   Undo.
-  (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
+  (** Implicitly at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
   Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
   solve [eapply interpf_SmartVarVar; subst; eassumption].
   Undo.
diff --git a/test-suite/bugs/closed/bug_808_2411.v b/test-suite/bugs/closed/bug_808_2411.v
index 1169b2036b..9fe4c9d503 100644
--- a/test-suite/bugs/closed/bug_808_2411.v
+++ b/test-suite/bugs/closed/bug_808_2411.v
@@ -2,7 +2,7 @@ Section test.
 Variable n:nat.
 Lemma foo: 0 <= n.
 Proof.
-(* declaring an Axiom during a proof makes it immediatly
+(* declaring an Axiom during a proof makes it immediately
    usable, juste as a full Definition. *)
 Axiom bar : n = 1.
 rewrite bar.
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index 0d75d52a31..d2e6794c0b 100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
@@ -14,7 +14,7 @@
 (* 02110-1301 USA                                                     *)
 
 
-(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful.
+(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful.
 *)
 
 Require Export ZArith.
@@ -84,7 +84,7 @@ End projection.
 
 
 (*###########################################################################*)
-(* Declaring some realtions on natural numbers for stepl and stepr tactics.  *)
+(* Declaring some relations on natural numbers for stepl and stepr tactics.  *)
 (*###########################################################################*)
 
 Lemma le_stepl: forall x y z, le x y -> x=z -> le z y.
@@ -173,7 +173,7 @@ Qed.
 
 
 (*###########################################################################*)
-(* Declaring some realtions on integers for stepl and stepr tactics.         *)
+(* Declaring some relations on integers for stepl and stepr tactics.         *)
 (*###########################################################################*)
 
 Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index dcc8bd7165..29614c032a 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -209,7 +209,7 @@ Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun
 Check exists_mixed x y '(u,t), x+y=0/\u+t=0.
 Check exists_mixed x y '(z,t), x+y=0/\z+t=0.
 
-(* Check that intermediary let-in are inserted inbetween instances of
+(* Check that intermediary let-in are inserted in between instances of
    the repeated pattern *)
 Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder).
 Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0.
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 3c427237b4..69ed621877 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -14,7 +14,7 @@
 (* 02110-1301 USA                                                     *)
 
 
-(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful.
+(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful.
 *)
 
 Require Export ZArith.
@@ -84,7 +84,7 @@ End projection.
 
 
 (*###########################################################################*)
-(* Declaring some realtions on natural numbers for stepl and stepr tactics.  *)
+(* Declaring some relations on natural numbers for stepl and stepr tactics.  *)
 (*###########################################################################*)
 
 Lemma le_stepl: forall x y z, le x y -> x=z -> le z y.
@@ -173,7 +173,7 @@ Qed.
 
 
 (*###########################################################################*)
-(* Declaring some realtions on integers for stepl and stepr tactics.         *)
+(* Declaring some relations on integers for stepl and stepr tactics.         *)
 (*###########################################################################*)
 
 Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z.
diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
index 69fca48e24..ba6bf3bba2 100644
--- a/test-suite/success/Case15.v
+++ b/test-suite/success/Case15.v
@@ -20,7 +20,7 @@ Definition test (B : Boite) :=
   | boite false (n, m) => n + m
   end.
 
-(* Check lazyness of compilation ... future work
+(* Check laziness of compilation ... future work
 Inductive I : Set := c : (b:bool)(if b then bool else nat)->I.
 
 Check [x]
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 8d9edbd62d..b0398ca056 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -62,7 +62,7 @@ Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option n
 
 (* -------------------------------------------------------------------- *)
 (*   Example to test patterns matching on dependent families            *)
-(* This exemple extracted from the developement done by Nacira Chabane  *)
+(* This exemple extracted from the development done by Nacira Chabane  *)
 (* (equipe Paris 6)                                                     *)
 (* -------------------------------------------------------------------- *)
 
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 2f13b7c225..e96a5f9048 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -175,7 +175,7 @@ End HintCut.
 
 
 (* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *)
-(* e.g. those tactics when considering a goal with existential varibles *)
+(* e.g. those tactics when considering a goal with existential variables *)
 (* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *)
 (* See this Coq club post for more detail: *)
 (* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *)
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index ee540d7109..1dbeaf3e1f 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -179,7 +179,7 @@ exact Logic.I.
 Qed.
 
 (* Up to September 2014, H0 below was renamed called H1 because of a collision
-   with the automaticallly generated names for equations.
+   with the automatically generated names for equations.
    (example taken from CoLoR) *)
 
 Inductive term := Var | Fun : term -> term -> term.
diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v
index de9b997590..98759264e5 100644
--- a/test-suite/success/Reordering.v
+++ b/test-suite/success/Reordering.v
@@ -1,7 +1,7 @@
 (* Testing the reordering of hypothesis required by pattern, fold and change. *)
 Goal forall (A:Set) (x:A) (A':=A), True.
 intros.
-fold A' in x. (* suceeds: x is moved after A' *)
+fold A' in x. (* succeeds: x is moved after A' *)
 Undo.
 pattern A' in x.
 Undo.
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index fb0adabae9..c566a6db9f 100644
--- a/test-suite/success/extraction_dep.v
+++ b/test-suite/success/extraction_dep.v
@@ -34,7 +34,7 @@ Definition testAbis := Abis.u + Abis.y.
 Recursive Extraction testAbis. (* without: A B v w x *)
 Extraction TestCompile testAbis.
 
-(** 2) With signature, we only keep elements mentionned in signature. *)
+(** 2) With signature, we only keep elements mentioned in signature. *)
 
 Module Type SIG.
  Parameter u : nat.
diff --git a/test-suite/success/if.v b/test-suite/success/if.v
index c81d2b9bf1..68d26ac8df 100644
--- a/test-suite/success/if.v
+++ b/test-suite/success/if.v
@@ -1,4 +1,4 @@
-(* The synthesis of the elimination predicate may fail if algebric *)
+(* The synthesis of the elimination predicate may fail if algebraic *)
 (* universes are not cautiously treated *)
 
 Check (fun b : bool => if b then Type else nat).