diff --git a/theories/base.v b/theories/base.v
index 6f80b885ed9f45d41b318fd4fb0d8faefa9b319f..a3a8d2759fff859f1e731bd0e5bb7e2080dba787 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -258,7 +258,7 @@ Hint Mode LeibnizEquiv ! - : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
-Proof. split; [apply leibniz_equiv | intros ->; reflexivity]. Qed.
+Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
 
 Ltac fold_leibniz := repeat
   match goal with
diff --git a/theories/boolset.v b/theories/boolset.v
index d630688eb6b2acb1e55ef8f19ad82d077f5f3e33..0312b8683ad9ecf6817dafc155813d1859e00b74 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -22,8 +22,8 @@ Proof.
   split; [split; [split| |]|].
   - by intros x ?.
   - 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.
+  - 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.
     destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
   - done.
diff --git a/theories/coGset.v b/theories/coGset.v
index 6736e7ac9365ce13e961d1e5ffeedd7773479dfd..b8816667974f777580eddcb5716bd25f4c888da1 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -138,8 +138,9 @@ Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
 Lemma coGpick_elem_of `{Countable A, Infinite A} X :
   ¬set_finite X → coGpick X ∈ X.
 Proof.
-  unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
-  done. by intros _; apply is_fresh.
+  unfold coGpick.
+  destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
+  by intros _; apply is_fresh.
 Qed.
 
 (** * Conversion to and from gset *)
@@ -168,8 +169,8 @@ Definition coGset_to_coPset (X : coGset positive) : coPset :=
 Lemma elem_of_coGset_to_coPset X x : x ∈ coGset_to_coPset X ↔ x ∈ X.
 Proof.
   destruct X as [X|X]; simpl.
-  by rewrite elem_of_gset_to_coPset.
-  by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
+  - by rewrite elem_of_gset_to_coPset.
+  - by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
 Qed.
 
 (** * Inefficient conversion to arbitrary sets with a top element *)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 137c42db7e1caa12f786e737ddd9f2d36e760312..70cef3c48730ee95034c4158152d6b2bbca840c1 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -234,7 +234,7 @@ End setoid.
 
 (** ** General properties *)
 Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i.
-Proof. split. by intros ->. apply map_eq. Qed.
+Proof. split; [by intros ->|]. apply map_eq. Qed.
 Lemma map_subseteq_spec {A} (m1 m2 : M A) :
   m1 ⊆ m2 ↔ ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
 Proof.
@@ -450,7 +450,11 @@ Lemma delete_empty {A} i : delete i (∅ : M A) = ∅.
 Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
 Lemma delete_commute {A} (m : M A) i j :
   delete i (delete j m) = delete j (delete i m).
-Proof. destruct (decide (i = j)). by subst. by apply partial_alter_commute. Qed.
+Proof.
+  destruct (decide (i = j)).
+  - by subst.
+  - by apply partial_alter_commute.
+Qed.
 Lemma delete_insert_ne {A} (m : M A) i j x :
   i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
 Proof. intro. by apply partial_alter_commute. Qed.
@@ -591,7 +595,7 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
   ∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
 Proof.
   intros Hi Hm1m2. exists (delete i m2). split_and?.
-  - rewrite insert_delete, insert_id. done.
+  - rewrite insert_delete, insert_id; [done|].
     eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert.
   - eauto using insert_delete_subset.
   - by rewrite lookup_delete.
@@ -876,7 +880,8 @@ Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
 Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
 Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
 Proof.
-  split. apply map_to_list_empty_inv. intros ->. apply map_to_list_empty.
+  split; [apply map_to_list_empty_inv|].
+  - intros ->. apply map_to_list_empty.
 Qed.
 
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :
@@ -982,7 +987,10 @@ Proof.
   unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty'.
 Qed.
 Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
-Proof. split. apply map_size_empty_inv. by intros ->; rewrite map_size_empty. Qed.
+Proof.
+  split; [apply map_size_empty_inv|].
+  by intros ->; rewrite map_size_empty.
+Qed.
 Lemma map_size_non_empty_iff {A} (m : M A) : size m ≠ 0 ↔ m ≠ ∅.
 Proof. by rewrite map_size_empty_iff. Qed.
 
@@ -1703,7 +1711,7 @@ Proof. by apply (partial_alter_merge _). Qed.
 Lemma foldr_delete_union_with (m1 m2 : M A) is :
   foldr delete (union_with f m1 m2) is =
     union_with f (foldr delete m1 is) (foldr delete m2 is).
-Proof. induction is as [|?? IHis]; simpl. done. by rewrite IHis, delete_union_with. Qed.
+Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_union_with. Qed.
 Lemma insert_union_with m1 m2 i x y z :
   f x y = Some z →
   <[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=y]>m2).
@@ -2065,7 +2073,7 @@ Proof. by apply (partial_alter_merge _). Qed.
 Lemma foldr_delete_intersection_with (m1 m2 : M A) is :
   foldr delete (intersection_with f m1 m2) is =
     intersection_with f (foldr delete m1 is) (foldr delete m2 is).
-Proof. induction is as [|?? IHis]; simpl. done. by rewrite IHis, delete_intersection_with. Qed.
+Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_intersection_with. Qed.
 Lemma insert_intersection_with m1 m2 i x y z :
   f x y = Some z →
   <[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2).
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index fc12d84fb74cdcb1d6b491121407a8c6816e3b4c..3778161516a669db75a657e0d673b42800e4439c 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -125,7 +125,7 @@ Proof.
   by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
 Qed.
 Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
-Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
+Proof. split; [apply size_empty_inv|]. by intros ->; rewrite size_empty. Qed.
 Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
 Proof. by rewrite size_empty_iff. Qed.
 
@@ -198,7 +198,7 @@ Proof.
   { apply set_wf. }
   intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
   - rewrite (union_difference {[ x ]} X) by set_solver.
-    apply Hadd. set_solver. apply IH; set_solver.
+    apply Hadd; [set_solver|]. apply IH; set_solver.
   - by rewrite HX.
 Qed.
 Lemma set_ind_L `{!LeibnizEquiv C} (P : C → Prop) :
@@ -217,10 +217,10 @@ Proof.
     symmetry. apply elem_of_elements. }
   induction 1 as [|x l ?? IH]; simpl.
   - intros X HX. setoid_rewrite elem_of_nil in HX.
-    rewrite equiv_empty. done. set_solver.
+    rewrite equiv_empty; [done|]. set_solver.
   - intros X HX. setoid_rewrite elem_of_cons in HX.
     rewrite (union_difference {[ x ]} X) by set_solver.
-    apply Hadd. set_solver. apply IH. set_solver.
+    apply Hadd; [set_solver|]. apply IH; set_solver.
 Qed.
 Lemma set_fold_ind_L `{!LeibnizEquiv C}
     {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
diff --git a/theories/finite.v b/theories/finite.v
index 6431920e02a5430ec35e7c04182161bcdc205b32..3830977bf6359a22d84a2648a4251781433aae00 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -37,7 +37,9 @@ Proof.
   rewrite Nat2Pos.id by done; simpl.
   destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
   - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
-  - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
+  - destruct xs; simpl.
+    + exfalso; eapply not_elem_of_nil, (HA x).
+    + lia.
 Qed.
 Lemma encode_decode A `{finA: Finite A} i :
   i < card A → ∃ x : A, decode_nat i = Some x ∧ encode_nat x = i.
@@ -258,9 +260,9 @@ Proof. done. Qed.
 
 Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
 Next Obligation.
-  constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton.
+  constructor; [ by rewrite elem_of_list_singleton | apply NoDup_singleton ].
 Qed.
-Next Obligation. intros [|]. left. right; left. Qed.
+Next Obligation. intros [|]; [ left | right; left ]. Qed.
 Lemma bool_card : card bool = 2.
 Proof. done. Qed.
 
@@ -292,7 +294,7 @@ Next Obligation.
     rewrite elem_of_app, elem_of_list_fmap.
     intros [(?&?&?)|?]; simplify_eq.
     + destruct Hx. by left.
-    + destruct IH. by intro; destruct Hx; right. auto.
+    + destruct IH; [ | auto ]. by intro; destruct Hx; right.
   - done.
 Qed.
 Next Obligation.
@@ -335,7 +337,7 @@ Next Obligation.
   revert IH. generalize (list_enum (enum A) n). intros k Hk.
   induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
   - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
-    eexists (l↾Hl'). split. by apply (sig_eq_pi _). done.
+    eexists (l↾Hl'). split; [|done]. by apply (sig_eq_pi _).
   - rewrite elem_of_app. eauto.
 Qed.
 
diff --git a/theories/hashset.v b/theories/hashset.v
index 065c58b1931c0c662bc4db7788d83eb1cad24166..82bd138c0e2d73fe5152d769c2cd00066b9ec6b7 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -144,7 +144,9 @@ Qed.
 Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
 Proof.
   unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
-  apply NoDup_nil_2. apply NoDup_singleton. apply NoDup_elements.
+  - apply NoDup_nil_2.
+  - apply NoDup_singleton.
+  - apply NoDup_elements.
 Qed.
 Definition listset_normalize (X : listset A) : listset A :=
   let (l) := X in Listset (remove_dups_fast l).
diff --git a/theories/list.v b/theories/list.v
index 7ebf5859f025c4c46cbf3b8442c9f9e2699686a7..a0fa9d54fa31af628895a78dbbcb1b3105fd62e0 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2205,9 +2205,7 @@ Proof.
       - done.
       - by constructor. }
     destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
-    split.
-    + by constructor.
-    + by constructor.
+    split; [ by constructor | by constructor ].
   - intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
     { exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
       destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
@@ -2262,9 +2260,9 @@ Proof. intro. apply submseteq_Permutation_length_le. lia. Qed.
 Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@submseteq A).
 Proof.
   intros l1 l2 ? k1 k2 ?. split; intros.
-  - trans l1. { by apply Permutation_submseteq. }
+  - trans l1; [by apply Permutation_submseteq|].
     trans k1; [done|]. by apply Permutation_submseteq.
-  - trans l2. { by apply Permutation_submseteq. }
+  - trans l2; [by apply Permutation_submseteq|].
     trans k2; [done|]. by apply Permutation_submseteq.
 Qed.
 Global Instance: AntiSymm (≡ₚ) (@submseteq A).
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index a64bb73a05a0041b4cdc3a9015cc1debeeb151fb..9f9139ea76feb213c89c33f996a2c9c859d6a547 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -41,5 +41,5 @@ Qed.
 
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
 Global Instance listset_nodup_fin_set: FinSet A C.
-Proof. split. apply _. done. by intros [??]. Qed.
+Proof. split; [apply _|done|]. by intros [??]. Qed.
 End list_set.
diff --git a/theories/natmap.v b/theories/natmap.v
index 2b892d5a6a6f4317b3a609e2f20db6fbf471b81a..d53da944a3e85c2a4dd0ab80b9fa002e332fa966 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -195,7 +195,7 @@ Lemma natmap_map_wf {A B} (f : A → B) l :
   natmap_wf l → natmap_wf (natmap_map_raw f l).
 Proof.
   unfold natmap_map_raw, natmap_wf. rewrite fmap_last.
-  destruct (last l). by apply fmap_is_Some. done.
+  destruct (last l); [|done]. by apply fmap_is_Some.
 Qed.
 Lemma natmap_lookup_map_raw {A B} (f : A → B) i l :
   mjoin (natmap_map_raw f l !! i) = f <$> mjoin (l !! i).
@@ -215,8 +215,10 @@ Proof.
     + by specialize (E 0).
     + destruct (natmap_wf_lookup (None :: l2)) as (i&?&?); auto with congruence.
     + by specialize (E 0).
-    + f_equal. apply (E 0). apply IH; eauto using natmap_wf_inv.
-      intros i. apply (E (S i)).
+    + f_equal.
+      * apply (E 0).
+      * apply IH; eauto using natmap_wf_inv.
+        intros i. apply (E (S i)).
     + by specialize (E 0).
     + destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
     + by specialize (E 0).
diff --git a/theories/nmap.v b/theories/nmap.v
index 56b692f953ac21c568c1babc05656443b1c68225..fdf9fab5e380cf52181741d667239c9d7ae9a681 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -53,7 +53,7 @@ Proof.
   - intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
   - intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
     intros. apply lookup_partial_alter_ne. congruence.
-  - intros ??? [??] []; simpl. done. apply lookup_fmap.
+  - intros ??? [??] []; simpl; [done|]. apply lookup_fmap.
   - intros ? [[x|] t]; unfold map_to_list; simpl.
     + constructor.
       * rewrite elem_of_list_fmap. by intros [[??] [??]].
diff --git a/theories/numbers.v b/theories/numbers.v
index ff91aa1c1c7a8262e95e8314028160fc43fa4dd9..d1a2d1946e991a23b7a5ab31e57d6b3a495a13ae 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -373,7 +373,8 @@ Proof.
   intros [??] ?.
   destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
   destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
-  split. { apply Z.quot_pos; lia. } trans x; auto. apply Z.quot_lt; lia.
+  split; [apply Z.quot_pos; lia|].
+  trans x; auto. apply Z.quot_lt; lia.
 Qed.
 
 Arguments Z.pred : simpl never.
@@ -529,9 +530,8 @@ Proof.
 Qed.
 Instance Qc_lt_strict: StrictOrder (<).
 Proof.
-  split; red.
-  - intros x Hx. by destruct (Qclt_not_eq x x).
-  - apply Qclt_trans.
+  split; red; [|apply Qclt_trans].
+  intros x Hx. by destruct (Qclt_not_eq x x).
 Qed.
 Instance Qc_le_total: Total Qcle.
 Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.
@@ -846,9 +846,8 @@ Proof. rewrite Qcplus_comm. apply Qp_le_plus_r. Qed.
 
 Lemma Qp_le_plus_compat (q p n m : Qp) : q ≤ n → p ≤ m → q + p ≤ n + m.
 Proof.
-  intros. eapply Qcle_trans.
-  - by apply Qcplus_le_mono_l.
-  - by apply Qcplus_le_mono_r.
+  intros. eapply Qcle_trans; [by apply Qcplus_le_mono_l
+                             |by apply Qcplus_le_mono_r].
 Qed.
 
 Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o.
diff --git a/theories/pmap.v b/theories/pmap.v
index 211dce6482113dea710aed1877db65e113cca69f..3f507bd7d7d341f5455ae29ed55de59674d02079 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -294,7 +294,9 @@ Proof.
     intros ??. by rewrite elem_of_nil.
   - intros ? [??] i x; unfold map_to_list, Pto_list.
     rewrite Pelem_of_to_list, elem_of_nil.
-    split. by intros [(?&->&?)|]. by left; exists i.
+    split.
+    + by intros [(?&->&?)|].
+    + by left; exists i.
   - intros ?? ? [??] ?. by apply Pomap_lookup.
   - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
 Qed.
diff --git a/theories/relations.v b/theories/relations.v
index 6d8c1eb7e6c4471edf6c351056bbffdfdc2c4d32..e4543886bb2a7c002850714d24de130f8bdb4cd3 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -95,7 +95,7 @@ Section closure.
      See Coq bug https://github.com/coq/coq/issues/7916 and the test
      [tests.typeclasses.test_setoid_rewrite]. *)
   Global Instance rtc_po : PreOrder (rtc R) | 10.
-  Proof. split. exact (@rtc_refl A R). exact rtc_transitive. Qed.
+  Proof. split; [exact (@rtc_refl A R) | exact rtc_transitive]. Qed.
 
   (* Not an instance, related to the issue described above, this sometimes makes
   [setoid_rewrite] queries loop. *)
@@ -133,7 +133,7 @@ Section closure.
   Proof. revert z. apply rtc_ind_r; eauto. Qed.
 
   Lemma rtc_nf x y : rtc R x y → nf R x → x = y.
-  Proof. destruct 1 as [x|x y1 y2]. done. intros []; eauto. Qed.
+  Proof. destruct 1 as [x|x y1 y2]; [done|]. intros []; eauto. Qed.
 
   Lemma rtc_congruence {B} (f : A → B) (R' : relation B) x y :
     (∀ x y, R x y → R' (f x) (f y)) → rtc R x y → rtc R' (f x) (f y).