Fixing typos - Part 3

7 files changed, 7 insertions, 7 deletions

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).