diff --git a/theories/base.v b/theories/base.v
index 0e6fece31159b8d091f21082cb0d806b604ecc5e..c972c3f2ac04afd33e0740d31932fc87fea761b1 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1000,7 +1000,7 @@ Hint Mode UpClose - ! : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
-(** We define operational type classes for the monadic operations bind, join 
+(** We define operational type classes for the monadic operations bind, join
 and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
@@ -1106,7 +1106,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
-if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
+if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
diff --git a/theories/boolset.v b/theories/boolset.v
index 8a0d4c54f1b84b1396d60da9639e5ff5c2b2d150..d630688eb6b2acb1e55ef8f19ad82d077f5f3e33 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -24,7 +24,7 @@ Proof.
   - by intros x y; rewrite <-(bool_decide_spec (x = y)).
   - split. apply orb_prop_elim. apply orb_prop_intro.
   - split. apply andb_prop_elim. apply andb_prop_intro.
-  - intros X Y x; unfold elem_of, boolset_elem_of; simpl. 
+  - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
     destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
   - done.
 Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d8d65511501671fffe29ecb6bd1193b03d51f2c0..eaab32feb7025cae2b46a9310334c89233bdf04f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -41,7 +41,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
   elem_of_map_to_list {A} (m : M A) i x :
     (i,x) ∈ map_to_list m ↔ m !! i = Some x;
   lookup_omap {A B} (f : A → option B) (m : M A) i :
-    omap f m !! i = m !! i ≫= f; 
+    omap f m !! i = m !! i ≫= f;
   lookup_merge {A B C} (f : option A → option B → option C)
       `{!DiagNone f} (m1 : M A) (m2 : M B) i :
     merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 634b010a2fa1c7a3e6e051e93bb8fae3cb1987ac..f0fa7ffb1934914d064f3667e761df121d431a95 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -50,7 +50,7 @@ Section definitions.
 
   Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
     let (X) := X in dom _ X.
-End definitions. 
+End definitions.
 
 Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
 Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
diff --git a/theories/hashset.v b/theories/hashset.v
index cb1f86aafcdc815557952751f66d9a71c74bece6..ba2e173f54302fbdcff915eac88b7b0fc07a1420 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -29,7 +29,7 @@ Next Obligation.
 Qed.
 Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
-  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. 
+  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
 Next Obligation.
   intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
   intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto.
diff --git a/theories/lexico.v b/theories/lexico.v
index 8710637388a1a931c544517d353c1834b4e0a945..6c051421db29faadf31dea0dfd21cc48503d5601 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -141,7 +141,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
   (P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
 Proof.
   unfold lexico, sig_lexico. split.
-  - intros [x ?] ?. by apply (irreflexivity lexico x). 
+  - intros [x ?] ?. by apply (irreflexivity lexico x).
   - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
 Qed.
 Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
diff --git a/theories/list.v b/theories/list.v
index 2a2a79466b450cab3b15a94f9281b70a3d020cd8..0cb74cf52961b9585c90c539d38886b757790380 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -401,7 +401,7 @@ used by [positives_flatten]. *)
 Definition positives_unflatten (p : positive) : option (list positive) :=
   positives_unflatten_go p [] 1.
 
-(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] 
+(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
 over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
 Definition seqZ (m len: Z) : list Z :=
   (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
@@ -4144,7 +4144,7 @@ Section positives_flatten_unflatten.
       rewrite 2!(assoc_L (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_go_app p suffix xs acc :
     positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
     positives_unflatten_go suffix xs (acc ++ p).
@@ -4161,7 +4161,7 @@ Section positives_flatten_unflatten.
       reflexivity.
     - reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_flatten_go suffix xs acc :
     positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 =
     positives_unflatten_go suffix (xs ++ acc) 1.
@@ -4178,7 +4178,7 @@ Section positives_flatten_unflatten.
       rewrite (left_id_L 1 (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_flatten xs :
     positives_unflatten (positives_flatten xs) = Some xs.
   Proof.
@@ -4191,7 +4191,7 @@ Section positives_flatten_unflatten.
     rewrite (right_id_L [] (++)%list).
     reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_app xs ys :
     positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
   Proof.
@@ -4205,7 +4205,7 @@ Section positives_flatten_unflatten.
       rewrite (assoc_L (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_cons x xs :
     positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
   Proof.
@@ -4214,7 +4214,7 @@ Section positives_flatten_unflatten.
     rewrite (assoc_L (++)).
     reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_suffix (l k : list positive) :
     l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
   Proof.
@@ -4222,7 +4222,7 @@ Section positives_flatten_unflatten.
     exists (positives_flatten l').
     apply positives_flatten_app.
   Qed.
-  
+
   Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) :
     length xs = length ys →
     p1 ++ positives_flatten xs = p2 ++ positives_flatten ys →
diff --git a/theories/listset.v b/theories/listset.v
index c443682bac01f2bd0e3ff7160dd5ca0038a4530d..2e0e892cb663bcb2f98fed4402c8e8f9bf5c6b61 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -29,7 +29,7 @@ Proof.
   destruct X as [l]; split; [|by intros; simplify_eq/=].
   rewrite elem_of_equiv_empty; intros Hl.
   destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
-Qed. 
+Qed.
 Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
 Proof.
  refine (cast_if (decide (listset_car X = [])));
diff --git a/theories/numbers.v b/theories/numbers.v
index 44d57e3f60e7a7b621e7c727cf6da4b1e43bea3d..330dcf47080ce9c2e002c8cab26441611ff6fb04 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -213,7 +213,7 @@ Proof.
   - by rewrite Preverse_xO, Preverse_app, IH.
   - reflexivity.
 Qed.
-    
+
 Instance Preverse_inj : Inj (=) (=) Preverse.
 Proof.
   intros p q eq.
@@ -571,7 +571,7 @@ Proof.
   by apply Qcplus_le_mono_l.
 Qed.
 Lemma Qcplus_nonneg_pos (x y : Qc) : 0 ≤ x → 0 < y → 0 < x + y.
-Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. 
+Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
 Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
 Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
 Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
diff --git a/theories/sets.v b/theories/sets.v
index 3ecda91da667ad85456175b9391ee31c008a0ec0..5e63b40a023026af7934f06128946201db147e27 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -564,7 +564,7 @@ Section semi_set.
     Lemma union_list_reverse_L Xs : ⋃ (reverse Xs) = ⋃ Xs.
     Proof. unfold_leibniz. apply union_list_reverse. Qed.
     Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (.= ∅) Xs.
-    Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
+    Proof. unfold_leibniz. by rewrite empty_union_list. Qed.
   End leibniz.
 
   Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
@@ -604,7 +604,7 @@ Section set.
 
   (** Intersection *)
   Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X.
-  Proof. set_solver. Qed. 
+  Proof. set_solver. Qed.
   Lemma subseteq_intersection_1 X Y : X ⊆ Y → X ∩ Y ≡ X.
   Proof. apply subseteq_intersection. Qed.
   Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y.
diff --git a/theories/tactics.v b/theories/tactics.v
index 00e7f9af1dcbf3bb9edf902d2b5c490d3a470bdb..f9a13635ded1d863f8c9ce21ff5fe1ebbf82020a 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -520,7 +520,7 @@ Ltac find_pat pat tac :=
       tryif tac x then idtac else fail 2
   end.
 
-(** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
+(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on sets. The [naive_solver] tactic implements an
 ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking