diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index ccb061003a11268da2e5b9a0a00005785188da77..2c8165cf10bff603132c3f7e054bee0c1129537d 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -14,7 +14,7 @@ Local Arguments op _ _ _ !_ /.
 Local Arguments pcore _ _ !_ /.
 
 (* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type := 
+Inductive dec_agree (A : Type) : Type :=
   | DecAgree : A → dec_agree A
   | DecAgreeBot : dec_agree A.
 Arguments DecAgree {_} _.
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index dc459baf45b763368a8be51d8773630aef0541e4..e2f3faf7d5ffed1391a1d267f1679d36dfd4b807 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -22,7 +22,7 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   mixin_dra_core_disjoint_l x : ✓ x → core x ## x;
   mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
   mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_mono x y : 
+  mixin_dra_core_mono x y :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z
 }.
 Structure draT := DraT {
@@ -81,7 +81,7 @@ Section dra_mixin.
   Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
   Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
   Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_mono x y : 
+  Lemma dra_core_mono x y :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z.
   Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
 End dra_mixin.
@@ -209,7 +209,7 @@ Proof.
     assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
     split; first done. exists (to_validity z). split; first split.
     + intros _. simpl. by split_and!.
-    + intros _. setoid_subst. by apply dra_op_valid. 
+    + intros _. setoid_subst. by apply dra_op_valid.
     + intros _. rewrite /= EQ //.
 Qed.
 *)
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index a0fd519b00d28b13f1a2587cd4b7c4acd91a7cdd..62c200d3a29649b1308a1423ad35d271e19057ca 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -8,7 +8,7 @@ Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Instance: Params (@ofe_fun_insert) 5.
 
-Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT} 
+Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT}
   (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
 Instance: Params (@ofe_fun_singleton) 5.
 
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d573744c283d7a6106d6166ddf434deaf02f62ae..7810042a61a57f1de308b0e593d3aedb71acf6a6 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
     category, and mathematically speaking, the entire development lives
     in this category. However, we will generally prefer to work with raw
     Coq functions plus some registered Proper instances for non-expansiveness.
-    This makes writing such functions much easier. It turns out that it many 
+    This makes writing such functions much easier. It turns out that it many
     cases, we do not even need non-expansiveness.
 *)
 
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 66e4726e9c67e57f4b690e5930614bac087009c9..ceff0397934627149df817093562036da6ddebe0 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -311,7 +311,7 @@ Proof. done. Qed.
 Lemma sts_frag_up_valid s T : ✓ sts_frag_up s T ↔ tok s ## T.
 Proof.
   split.
-  - move=>/sts_frag_valid [H _]. apply H, elem_of_up. 
+  - move=>/sts_frag_valid [H _]. apply H, elem_of_up.
   - intros. apply sts_frag_valid; split. by apply closed_up. set_solver.
 Qed.
 
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index edc4289c05a70fac9355a28bbd594a146c9972ee..a57b61357380c0f2ccaccf16c6cfacd2fc277e8c 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -228,7 +228,7 @@ Proof.
   revert P.
   induction k; intros P.
   - rewrite //= ?right_id. apply wand_intro_l.
-    rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r. 
+    rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r.
   - rewrite {2}(nnupd_k_unfold k P).
     apply and_intro.
     * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
@@ -291,9 +291,9 @@ Qed.
 End classical.
 
 (* We might wonder whether we can prove an adequacy lemma for nnupd. We could combine
-   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but 
+   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but
    this would rely on the classical axiom we needed to prove the equivalence! Can
-   we establish adequacy without axioms? Unfortunately not, because adequacy for 
+   we establish adequacy without axioms? Unfortunately not, because adequacy for
    nnupd would imply double negation elimination, which is classical: *)
 
 Lemma nnupd_dne φ: (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I.
@@ -327,7 +327,7 @@ Proof.
     intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
     unseal.
     assert (n' < S k ∨ n' = S k) as [|] by omega.
-    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall. 
+    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
       eapply Hsmall; eauto.
     * subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
   - intros k P x Hx. rewrite ?Nat_iter_S_r.
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index dc226f276d5a29ec5eaf26085ca33c4bda87d040..dfee3989ab332b4ead7a05ac10f912363991ba5a 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -84,7 +84,7 @@ End namespace.
 
 (* The hope is that registering these will suffice to solve most goals
 of the forms:
-- [N1 ## N2] 
+- [N1 ## N2]
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Create HintDb ndisj.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 00ddee6e6cea01022541fe0628533cbc0c0b3c0c..0d8e8ced6b615324537aded18038145a6d64606b 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -82,7 +82,7 @@ Section sts.
     sts_own γ s1 T ==∗ sts_own γ s2 T.
   Proof.
     intros ??. apply own_update, sts_update_frag_up; [|done..].
-    intros Hdisj. apply sts.closed_up. done. 
+    intros Hdisj. apply sts.closed_up. done.
   Qed.
 
   Lemma sts_own_weaken_tok γ s T1 T2 :
diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v
index 717bcec14f9d80be7a7455ff8b6d90edc8eb45a7..49085be989a91b7b36a51a6dfb470d3cb663aafe 100644
--- a/theories/base_logic/tactics.v
+++ b/theories/base_logic/tactics.v
@@ -60,7 +60,7 @@ Module uPred_reflection. Section uPred_reflection.
     match e with
     | ETrue => None
     | EVar n' => if decide (n = n') then Some ETrue else None
-    | ESep e1 e2 => 
+    | ESep e1 e2 =>
        match cancel_go n e1 with
        | Some e1' => Some (ESep e1' e2)
        | None => ESep e1 <$> cancel_go n e2
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 45f540eceb521c8268ac27054fa2720bbb402d86..39c6625fdc323eade1a7311b09c19a45056f1d16 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -276,7 +276,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
-  | StoreLCtx e2 => Store e e2 
+  | StoreLCtx e2 => Store e e2
   | StoreRCtx v1 => Store (of_val v1) e
   | CasLCtx e1 e2 => CAS e e1 e2
   | CasMCtx v0 e2 => CAS (of_val v0) e e2
@@ -365,11 +365,11 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
      head_step (App (Rec f x e1) e2) σ e' σ []
   | UnOpS op e v v' σ :
      to_val e = Some v →
-     un_op_eval op v = Some v' → 
+     un_op_eval op v = Some v' →
      head_step (UnOp op e) σ (of_val v') σ []
   | BinOpS op e1 e2 v1 v2 v' σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     bin_op_eval op v1 v2 = Some v' → 
+     bin_op_eval op v1 v2 = Some v' →
      head_step (BinOp op e1 e2) σ (of_val v') σ []
   | IfTrueS e1 e2 σ :
      head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index b9632c00c56c77d877d82dc6294721e44be25a74..8aee1924bb7256c1691f78a3bdf35e523f97017c 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -55,7 +55,7 @@ Section mono_proof.
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_valid_discrete_2.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply auth_update, (mnat_local_update _ _ (S c)); auto. } 
+      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
       wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 7437f74833d1af6324e16db7e7080036bf757e16..b75704bb0439af170769225ce8d32eb03941a948 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -94,7 +94,7 @@ Section proof.
       + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
         iModIntro. wp_let. wp_op. case_bool_decide; [|done].
-        wp_if. 
+        wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
@@ -129,7 +129,7 @@ Section proof.
       iModIntro. wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
-      + by iNext. 
+      + by iNext.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 677f071d729775ae8f35c0521e86e57fd6cff52c..e081ea449dc7bd80198541916a14470d4064ab49 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -237,7 +237,7 @@ Proof.
   iSplitL "He2"; first by iApply ("IH" with "He2"). iClear "Hred Hstep".
   induction efs as [|ef efs IH]; first by iApply big_sepL_nil.
   rewrite !big_sepL_cons. iDestruct "Hefs" as "(Hef & Hefs)".
-  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH. 
+  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH.
 Qed.
 
 Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 9497be34506b4e7f20a132cc2a9f892aeefffdbb..159a09b5ae02e28cbbfdc268f2704109535a512a 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -27,7 +27,7 @@ Definition ascii_beq (x y : ascii) : bool :=
     beq x5 y5 && beq x6 y6 && beq x7 y7 && beq x8 y8.
 
 Fixpoint string_beq (s1 s2 : string) : bool :=
-  match s1, s2 with 
+  match s1, s2 with
   | "", "" => true
   | String a1 s1, String a2 s2 => ascii_beq a1 a2 && string_beq s1 s2
   | _, _ => false
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index d980e776fed0384f999a229883869dceb507f82d..4816f938a0daae36ba3b2bcd964b00bb3936b3a9 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -40,7 +40,7 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
   match Γapp with
   | Enil => Some Γ
   | Esnoc Γapp i x =>
-     Γ' ← env_app Γapp Γ; 
+     Γ' ← env_app Γapp Γ;
      match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
   end.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ffa7bd43878e09a06b8287dd4b08c8f7c9317c20..315d0dccc9a885be5f3dabf85e8a23c8fa72b7c1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -327,14 +327,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   first
   [ (* (?P → _) *)
     eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [apply _ || 
+      [apply _ ||
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | (* (?P -∗ _) *)
     eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [apply _ || 
+      [apply _ ||
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"