Fixing typos - Part 3

8 files changed, 8 insertions, 8 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.