diff --git a/stdpp/base.v b/stdpp/base.v
index 73a43ae55c64dd0309275b43b07d0a72b64b329f..26fff8e206da17cb4a552bf1e09f482410e670c5 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1302,8 +1302,8 @@ Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 (* Defining a generic notation does not seem possible with Coq's
    recursive notation system, so we define individual notations
    for some cases relevant in practice. *)
-(* The "format" makes sure that linebreaks are placed after the separating semicola [;] when printing. *)
-(* TODO : we are using parantheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
+(* The "format" makes sure that linebreaks are placed after the separating semicolons [;] when printing. *)
+(* TODO : we are using parentheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
    and earlier have trouble with using the notation for printing otherwise.
    Once support for Coq 8.12 is dropped, this can be replaced with [$]. *)
 Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
@@ -1586,17 +1586,17 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
 }.
 
 (** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
-It contains a function [fresh : list A → A] that given a list [xs] gives an
+It contains a function [fresh : list A → A] that, given a list [xs], gives an
 element [fresh xs ∉ xs].
 
 We do not directly make [fresh] a field of the [Infinite] class, but use a
 separate operational type class [Fresh] for it. That way we can overload [fresh]
-to pick fresh elements from other data structure like sets. See the file
+to pick fresh elements from other data structures like sets. See the file
 [fin_sets], where we define [fresh : C → A] for any finite set implementation
 [FinSet C A].
 
 Note: we require [fresh] to respect permutations, which is needed to define the
-aforementioned [fresh] function on finite sets that respects set equality.
+aforementioned [fresh] function on finite sets that respect set equality.
 
 Instead of instantiating [Infinite] directly, consider using [max_infinite] or
 [inj_infinite] from the [infinite] module. *)
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index 309f308936e2abac063e35971a760c82dc6f6bd3..ea5c443a55379cc0d66cf25c52c128e2cf437481 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -52,7 +52,7 @@ Global Arguments GNode101 {A P} _ _ : assert.
 Global Arguments GNode110 {A P} _ _ _ : assert.
 Global Arguments GNode111 {A P} _ _ _ _ : assert.
 
-(** Using [Variant] we supress the generation of the induction scheme. We use
+(** Using [Variant] we suppress the generation of the induction scheme. We use
 the induction scheme [gmap_ind] in terms of the smart constructors to reduce the
 number of cases, similar to Appel and Leroy. *)
 Variant gmap_dep (A : Type) (P : positive → Prop) :=
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index d7fcff4068828741df23860f1aedd40231ab6042..7d62b6df6d1ee28f7ff19853dcc06f8df2ccfb2a 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -183,11 +183,11 @@ instantiates universally quantified hypotheses [H : ∀ x : A, P x] in two ways:
   in [H], so variable [x].
 
 Step (4) is implemented using the tactic [multiset_simplify_singletons], which
-simplifies occurences of [multiplicity x {[ y ]}] as follows:
+simplifies occurrences of [multiplicity x {[ y ]}] as follows:
 
 - First, we try to turn these occurencess into [1] or [0] if either [x = y] or
   [x ≠ y] can be proved using [done], respectively.
-- Second, we try to turn these occurences into a fresh [z ≤ 1] if [y] does not
+- Second, we try to turn these occurrences into a fresh [z ≤ 1] if [y] does not
   occur elsewhere in the hypotheses or goal.
 - Finally, we make a case distinction between [x = y] or [x ≠ y]. This step is
   done last so as to avoid needless exponential blow-ups.
@@ -313,7 +313,7 @@ Ltac multiset_instantiate :=
   end.
 
 (** Step 4: simplify singletons *)
-(** This lemma results in information loss if there are other occurences of
+(** This lemma results in information loss if there are other occurrences of
 [y] in the goal. In the tactic [multiset_simplify_singletons] we use [clear y]
 to ensure we do not use the lemma if it leads to information loss. *)
 Local Lemma multiplicity_singleton_forget `{Countable A} x y :
diff --git a/stdpp/list.v b/stdpp/list.v
index b3a076c436d6b579b2599f22a1c64f1a072238e4..5259b0ff6d56cca229b1ebb244956609e4cc7284 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -316,7 +316,7 @@ Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
 Global Hint Extern 0 (_ `sublist_of` _) => reflexivity : core.
 
 (** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
-from [l1] while possiblity changing the order. *)
+from [l1] while possibly changing the order. *)
 Inductive submseteq {A} : relation (list A) :=
   | submseteq_nil : submseteq [] []
   | submseteq_skip x l1 l2 : submseteq l1 l2 → submseteq (x :: l1) (x :: l2)
diff --git a/stdpp/pmap.v b/stdpp/pmap.v
index e14072db49cf49a54b737eba311383b3720e4e8a..109c0d7027121d13b1a41e145a503ffb43ce8d8a 100644
--- a/stdpp/pmap.v
+++ b/stdpp/pmap.v
@@ -38,7 +38,7 @@ Global Arguments PNode101 {A} _ _ : assert.
 Global Arguments PNode110 {A} _ _ : assert.
 Global Arguments PNode111 {A} _ _ _ : assert.
 
-(** Using [Variant] we supress the generation of the induction scheme. We use
+(** Using [Variant] we suppress the generation of the induction scheme. We use
 the induction scheme [Pmap_ind] in terms of the smart constructors to reduce the
 number of cases, similar to Appel and Leroy. *)
 Variant Pmap (A : Type) := PEmpty : Pmap A | PNodes : Pmap_ne A → Pmap A.
diff --git a/stdpp/sets.v b/stdpp/sets.v
index 7957836fbdbc127c9f4c1e684396d4e6e7b72c6f..9709dc45432da46bce94ae84733a00bc51a309a2 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -95,7 +95,7 @@ involving just [∈]. For example, [A → x ∈ X ∪ ∅] becomes [A → x ∈
 
 This transformation is implemented using type classes instead of setoid
 rewriting to ensure that we traverse each term at most once and to be able to
-deal with occurences of the set operations under binders. *)
+deal with occurrences of the set operations under binders. *)
 Class SetUnfold (P Q : Prop) := { set_unfold : P ↔ Q }.
 Global Arguments set_unfold _ _ {_} : assert.
 Global Hint Mode SetUnfold + - : typeclass_instances.
diff --git a/stdpp/strings.v b/stdpp/strings.v
index 8c59f0f36ab25edaf888897ddce4a62b3dae166b..0e70e2b4c3155762c40aacd7b5888e4b78938831 100644
--- a/stdpp/strings.v
+++ b/stdpp/strings.v
@@ -75,7 +75,7 @@ to be used as keys in [gmap].
 
 The encoding of [string] to [positive] is taken from
 https://github.com/xavierleroy/canonical-binary-tries/blob/v2/lib/String2pos.v.
-It avoids creating auxilary data structures such as [list bool], thereby
+It avoids creating auxiliary data structures such as [list bool], thereby
 improving efficiency. *)
 Local Definition bool_cons_pos (b : bool) (p : positive) : positive :=
   if b then p~1 else p~0.
@@ -99,7 +99,7 @@ The lemma [string_of_to_pos] ensures the generated definition is correct.
 
 Alternatively, we could implement it in two steps. Convert the [positive] to
 [list bool], and convert the list to [string]. This definition will be slower
-since auxilary data structures are created. *)
+since auxiliary data structures are created. *)
 Local Fixpoint pos_to_string (p : positive) : string.
 Proof.
   (** The argument [p] is the [positive] that we are peeling off.
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index f3639f00c03794d262d6016343f6fbfb1ef628dc..f838bf02249f22bd8a5e01f2f62d1a89d7071314 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -558,7 +558,7 @@ Ltac intros_revert tac :=
   end.
 
 (** The tactic [iter tac l] runs [tac x] for each element [x ∈ l] until [tac x]
-succeeds. If it does not suceed for any element of the generated list, the whole
+succeeds. If it does not succeed for any element of the generated list, the whole
 tactic wil fail. *)
 Tactic Notation "iter" tactic(tac) tactic(l) :=
   let rec go l :=
diff --git a/stdpp_bitvector/tactics.v b/stdpp_bitvector/tactics.v
index ba5fb63ac07a6cc44339e240775f4e7dde5740fa..b95c2102d41a3afff10257793963ffd219ae62d3 100644
--- a/stdpp_bitvector/tactics.v
+++ b/stdpp_bitvector/tactics.v
@@ -117,7 +117,7 @@ Class BvUnfold (n : N) (signed : bool) (wrapped : bool) (b : bv n) (z : Z) := {
 Global Arguments bv_unfold_proof {_ _ _} _ _ {_}.
 Global Hint Mode BvUnfold + + + + - : bv_unfold_db.
 
-(** [BV_UNFOLD_BLOCK] is a marker that this occurence of [bv_signed]
+(** [BV_UNFOLD_BLOCK] is a marker that this occurrence of [bv_signed]
 or [bv_unsigned] has already been simplified. *)
 Definition BV_UNFOLD_BLOCK {A} (x : A) : A := x.
 
diff --git a/tests/decidable.v b/tests/decidable.v
index b586ba75377ccfd45bf436fe017e6cac5676f246..8962e55f996b8a17d6fe3e48553523922d9c572c 100644
--- a/tests/decidable.v
+++ b/tests/decidable.v
@@ -6,6 +6,6 @@ Example issue_165 (x : nat) :
   ¬ ∃ xs : list nat, (guard (x ∈ xs);; Some x) ≠ None.
 Proof.
   intros [xs Hxs]. case_guard; [|done].
-  Fail done. (* Would succeed if the instance backing [x ∈ xs] is infered as
+  Fail done. (* Would succeed if the instance backing [x ∈ xs] is inferred as
   [False]. *)
 Abort.