Make bulleting strict for algebra and base_logic

theories/algebra/cmra.v

@@ -367,7 +367,7 @@ Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
 Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
 Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
-Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
+Proof. destruct my as [y|]; last done. move=> /(exclusiveN_l _ x) []. Qed.
 Lemma exclusive_includedN n x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
 Proof. intros [? ->]. by apply exclusiveN_l. Qed.
 Lemma exclusive_included x `{!Exclusive x} y : x ≼ y → ✓ y → False.
@@ -747,7 +747,7 @@ End cmra_total.
 
 (** * Properties about morphisms *)
 Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
-Proof. split=>//=. apply _. intros. by rewrite option_fmap_id. Qed.
+Proof. split=>//=; first apply _. intros. by rewrite option_fmap_id. Qed.
 Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CmraMorphism f} :
   Proper ((≡) ==> (≡)) f := ne_proper _.
 Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
@@ -1018,7 +1018,7 @@ Section discrete.
 
   Instance discrete_cmra_discrete :
     CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
-  Proof. split. apply _. done. Qed.
+  Proof. split; first apply _. done. Qed.
 End discrete.
 
 (** A smart constructor for the discrete RA over a carrier [A]. It uses
@@ -1192,7 +1192,7 @@ Section prod.
 
   Global Instance prod_cmra_discrete :
     CmraDiscrete A → CmraDiscrete B → CmraDiscrete prodR.
-  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
+  Proof. split; [apply _|]. by intros ? []; split; apply cmra_discrete_valid. Qed.
 
   (* FIXME(Coq #6294): This is not an instance because we need it to use the new
   unification. *)
@@ -1425,7 +1425,7 @@ Section option.
 
   Instance option_unit : Unit (option A) := None.
   Lemma option_ucmra_mixin : UcmraMixin optionR.
-  Proof. split. done. by intros []. done. Qed.
+  Proof. split; [ done | by intros [] | done ]. Qed.
   Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
 
   (** Misc *)
@@ -1456,13 +1456,13 @@ Section option.
 
   Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
     ✓{n} (Some a ⋅ mb) → mb = None.
-  Proof. destruct mb. move=> /(exclusiveN_l _ a) []. done. Qed.
+  Proof. destruct mb; [|done]. move=> /(exclusiveN_l _ a) []. Qed.
   Lemma exclusiveN_Some_r n a `{!Exclusive a} mb :
     ✓{n} (mb ⋅ Some a) → mb = None.
   Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
 
   Lemma exclusive_Some_l a `{!Exclusive a} mb : ✓ (Some a ⋅ mb) → mb = None.
-  Proof. destruct mb. move=> /(exclusive_l a) []. done. Qed.
+  Proof. destruct mb; [|done]. move=> /(exclusive_l a) []. Qed.
   Lemma exclusive_Some_r a `{!Exclusive a} mb : ✓ (mb ⋅ Some a) → mb = None.
   Proof. rewrite comm. by apply exclusive_Some_l. Qed.
 
@@ -1474,9 +1474,9 @@ Section option.
   Proof. rewrite Some_included; eauto. Qed.
 
   Lemma Some_includedN_total `{CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
-  Proof. rewrite Some_includedN. split. by intros [->|?]. eauto. Qed.
+  Proof. rewrite Some_includedN. split; [|eauto]. by intros [->|?]. Qed.
   Lemma Some_included_total `{CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
-  Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
+  Proof. rewrite Some_included. split; [|eauto]. by intros [->|?]. Qed.
 
   Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
     Some a ≼{n} Some b → ✓{n} b → a ≡{n}≡ b.

theories/algebra/cmra_big_op.v

@@ -8,7 +8,7 @@ Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
 Proof.
   revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
   - intros [??] [|k] y ?; naive_solver.
-  - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)).
+  - intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
 Qed.
 Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.

theories/algebra/coPset.v

@@ -43,7 +43,7 @@ Section coPset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma coPset_ucmra_mixin : UcmraMixin coPset.
-  Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
+  Proof. split; [done | | done]. intros X. by rewrite coPset_op_union left_id_L. Qed.
   Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
 
   Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -56,7 +56,7 @@ Section coPset.
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite coPset_op_union. set_solver.
+    split; [done|]. rewrite coPset_op_union. set_solver.
   Qed.
 End coPset.
 

theories/algebra/csum.v

@@ -349,7 +349,7 @@ Proof.
   intros Hup n mf ? Ha1; simpl in *.
   destruct (Hup n (mf ≫= maybe Cinl)); auto.
   { by destruct mf as [[]|]; inversion_clear Ha1. }
-  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
+  split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
 Lemma csum_local_update_r (b1 b2 b1' b2' : B) :
   (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2').
@@ -357,7 +357,7 @@ Proof.
   intros Hup n mf ? Ha1; simpl in *.
   destruct (Hup n (mf ≫= maybe Cinr)); auto.
   { by destruct mf as [[]|]; inversion_clear Ha1. }
-  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
+  split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
 End cmra.
 

theories/algebra/excl.v

@@ -82,7 +82,7 @@ Proof.
   split; try discriminate.
   - by intros n []; destruct 1; constructor.
   - by destruct 1; intros ?.
-  - intros x; split. done. by move=> /(_ 0).
+  - intros x; split; [done|]. by move=> /(_ 0).
   - intros n [?|]; simpl; auto with lia.
   - by intros [?|] [?|] [?|]; constructor.
   - by intros [?|] [?|]; constructor.
@@ -92,7 +92,7 @@ Qed.
 Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
 
 Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
-Proof. split. apply _. by intros []. Qed.
+Proof. split; first apply _. by intros []. Qed.
 
 (** Exclusive *)
 Global Instance excl_exclusive x : Exclusive x.

theories/algebra/functions.v

@@ -62,7 +62,10 @@ Section cmra.
 
   Global Instance discrete_fun_singleton_ne x :
     NonExpansive (discrete_fun_singleton x : B x → _).
-  Proof. intros n y1 y2 ?; apply discrete_fun_insert_ne. done. by apply equiv_dist. Qed.
+  Proof.
+    intros n y1 y2 ?; apply discrete_fun_insert_ne; [done|].
+    by apply equiv_dist.
+  Qed.
   Global Instance discrete_fun_singleton_proper x :
     Proper ((≡) ==> (≡)) (discrete_fun_singleton x) := ne_proper _.
 

theories/algebra/gmap.v

@@ -243,7 +243,11 @@ Implicit Types x y : A.
 
 Global Instance lookup_op_homomorphism i :
   MonoidHomomorphism op op (≡) (lookup i : gmap K A → option A).
-Proof. split; [split|]; try apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
+Proof.
+  split; [split|]; try apply _.
+  - intros m1 m2; by rewrite lookup_op.
+  - done.
+Qed.
 
 Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (.!! i)).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
@@ -261,7 +265,7 @@ Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
 Proof.
   split.
   - move=>/(_ i); by simplify_map_eq.
-  - intros. apply insert_validN. done. apply: ucmra_unit_validN.
+  - intros. apply insert_validN; first done. apply: ucmra_unit_validN.
 Qed.
 Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
 Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
@@ -311,7 +315,7 @@ Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hi.
     exists (x ⋅? m' !! i). rewrite -Some_op_opM.
-    split. done. apply cmra_includedN_l.
+    split; first done. apply cmra_includedN_l.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
@@ -324,7 +328,7 @@ Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
     exists (x ⋅? m' !! i). rewrite -Some_op_opM.
-    split. done. apply cmra_included_l.
+    split; first done. apply cmra_included_l.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.

theories/algebra/gmultiset.v

@@ -47,7 +47,7 @@ Section gmultiset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
-  Proof. split. done. intros X. by rewrite gmultiset_op_disj_union left_id_L. done. Qed.
+  Proof. split; [done | | done]. intros X. by rewrite gmultiset_op_disj_union left_id_L. Qed.
   Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
 
   Global Instance gmultiset_cancelable X : Cancelable X.

theories/algebra/gset.v

@@ -37,7 +37,7 @@ Section gset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma gset_ucmra_mixin : UcmraMixin (gset K).
-  Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
+  Proof. split; [ done | | done ]. intros X. by rewrite gset_op_union left_id_L. Qed.
   Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
 
   Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -50,7 +50,7 @@ Section gset.
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite gset_op_union. set_solver.
+    split; [done|]. rewrite gset_op_union. set_solver.
   Qed.
 
   Global Instance gset_core_id X : CoreId X.
@@ -164,7 +164,7 @@ Section gset_disj.
       (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
     Proof.
       intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
-      intros Y ?; exists (fresh Y). split. apply is_fresh. done.
+      intros Y ?; exists (fresh Y). split; [|done]. apply is_fresh.
     Qed.
     Lemma gset_disj_alloc_updateP' X :
       GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.

theories/algebra/lib/frac_auth.v

@@ -78,7 +78,8 @@ Section frac_auth.
   Lemma frac_auth_auth_validN n a : ✓{n} (●F a) ↔ ✓{n} a.
   Proof.
     rewrite auth_auth_frac_validN Some_validN. split.
-    by intros [?[]]. intros. by split.
+    - by intros [?[]].
+    - intros. by split.
   Qed.
   Lemma frac_auth_auth_valid a : ✓ (●F a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.

theories/algebra/lib/gmap_view.v

@@ -298,11 +298,11 @@ Section lemmas.
       { destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
         specialize (Hrel _ _ Hbf). destruct Hrel as (v' & _ & _ & Hm).
         exfalso. rewrite Hm in Hfresh. done. }
-      rewrite lookup_singleton Hbf right_id.
+      rewrite lookup_singleton Hbf right_id_L.
       intros [= <- <-]. eexists. do 2 (split; first done).
       rewrite lookup_insert. done.
     - rewrite lookup_singleton_ne; last done.
-      rewrite left_id=>Hbf.
+      rewrite left_id_L=>Hbf.
       specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & ? & Hm).
       eexists. do 2 (split; first done).
       rewrite lookup_insert_ne //.
@@ -336,14 +336,14 @@ Section lemmas.
         rewrite Hbf. clear Hbf.
         rewrite -Some_op -pair_op.
         move=>[/= /dfrac_full_exclusive Hdf _]. done. }
-      rewrite Hbf right_id lookup_singleton. clear Hbf.
+      rewrite Hbf right_id_L lookup_singleton. clear Hbf.
       intros [= <- <-].
       eexists. do 2 (split; first done).
       rewrite lookup_insert. done.
     - rewrite lookup_singleton_ne; last done.
-      rewrite left_id=>Hbf.
+      rewrite left_id_L=>Hbf.
       edestruct (Hrel j) as (v'' & ? & ? & Hm).
-      { rewrite lookup_op lookup_singleton_ne // left_id. done. }
+      { rewrite lookup_op lookup_singleton_ne // left_id_L. done. }
       simpl in *. eexists. do 2 (split; first done).
       rewrite lookup_insert_ne //.
   Qed.
@@ -367,9 +367,9 @@ Section lemmas.
         apply cmra_discrete_valid_iff. done.
       + simpl in *. move:Hbf=>[= <- <-]. split; done.
     - rewrite lookup_singleton_ne //.
-      rewrite left_id=>Hbf.
+      rewrite left_id_L=>Hbf.
       edestruct (Hrel j) as (v'' & ? & ? & Hm).
-      { rewrite lookup_op lookup_singleton_ne // left_id. done. }
+      { rewrite lookup_op lookup_singleton_ne // left_id_L. done. }
       simpl in *. eexists. do 2 (split; first done). done.
   Qed.
 

theories/algebra/lib/ufrac_auth.v

@@ -96,15 +96,24 @@ Section ufrac_auth.
   Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U{q} a) ↔ ✓{n} a.
   Proof.
     rewrite auth_auth_frac_validN Some_validN. split.
-    by intros [?[]]. intros. by split.
+    - by intros [?[]].
+    - intros. by split.
   Qed.
   Lemma ufrac_auth_auth_valid q a : ✓ (●U{q} a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
 
   Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U{q} a) ↔ ✓{n} a.
-  Proof. rewrite auth_frag_validN. split. by intros [??]. by split. Qed.
+  Proof.
+    rewrite auth_frag_validN. split.
+    - by intros [??].
+    - by split.
+  Qed.
   Lemma ufrac_auth_frag_valid q a : ✓ (◯U{q} a) ↔ ✓ a.
-  Proof. rewrite auth_frag_valid. split. by intros [??]. by split. Qed.
+  Proof.
+    rewrite auth_frag_valid. split.
+    - by intros [??].
+    - by split.
+  Qed.
 
   Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2.
   Proof. done. Qed.

theories/algebra/local_updates.v

@@ -187,5 +187,5 @@ Proof.
   move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
   destruct z as [z|]; last done. exfalso.
   move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
-  eapply cmra_validN_le. eapply Hy. lia.
+  eapply cmra_validN_le; [|lia]. eapply Hy.
 Qed.

theories/algebra/namespace_map.v

@@ -170,7 +170,9 @@ Proof.
     intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
     intros i. move: (Hdisj i). rewrite lookup_op.
     case: (m1 !! i)=> [a|]; last auto.
-    move=> []. by case: (m2 !! i). set_solver.
+    move=> [].
+    { by case: (m2 !! i). }
+    set_solver.
   - intros n x y1 y2 ? [??]; simpl in *.
     destruct (cmra_extend n (namespace_map_data_proj x)
       (namespace_map_data_proj y1) (namespace_map_data_proj y2))
@@ -195,7 +197,7 @@ Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
 Lemma namespace_map_ucmra_mixin : UcmraMixin (namespace_map A).
 Proof.
   split; simpl.
-  - rewrite namespace_map_valid_eq /=. split. apply ucmra_unit_valid. set_solver.
+  - rewrite namespace_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
   - split; simpl; [by rewrite left_id|by rewrite left_id_L].
   - do 2 constructor; [apply (core_id_core _)|done].
 Qed.
@@ -209,7 +211,7 @@ Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
 Lemma namespace_map_data_valid N a : ✓ (namespace_map_data N a) ↔ ✓ a.
 Proof. rewrite namespace_map_valid_eq /= singleton_valid. set_solver. Qed.
 Lemma namespace_map_token_valid E : ✓ (namespace_map_token E).
-Proof. rewrite namespace_map_valid_eq /=. split. done. by left. Qed.
+Proof. rewrite namespace_map_valid_eq /=. split; first done. by left. Qed.
 Lemma namespace_map_data_op N a b :
   namespace_map_data N (a ⋅ b) = namespace_map_data N a ⋅ namespace_map_data N b.
 Proof.

theories/algebra/ofe.v

@@ -203,7 +203,7 @@ Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
 Arguments dist_later _ _ !_ _ _ /.
 
 Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
-Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
+Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
 
 Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y → dist_later n x y.
 Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
@@ -279,7 +279,10 @@ Section limit_preserving.
   Lemma limit_preserving_and (P1 P2 : A → Prop) :
     LimitPreserving P1 → LimitPreserving P2 →
     LimitPreserving (λ x, P1 x ∧ P2 x).
-  Proof. intros Hlim1 Hlim2 c Hc. split. apply Hlim1, Hc. apply Hlim2, Hc. Qed.
+  Proof.
+    intros Hlim1 Hlim2 c Hc.
+    split; [ apply Hlim1, Hc | apply Hlim2, Hc ].
+  Qed.
 
   Lemma limit_preserving_impl (P1 P2 : A → Prop) :
     Proper (dist 0 ==> impl) P1 → LimitPreserving P2 →
@@ -662,8 +665,9 @@ Section product.
   Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
     { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
   Next Obligation.
-    intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
-    apply (conv_compl n (chain_map snd c)).
+    intros ?? n c; split.
+    - apply (conv_compl n (chain_map fst c)).
+    - apply (conv_compl n (chain_map snd c)).
   Qed.
 
   Global Instance prod_discrete (x : A * B) :
@@ -1096,7 +1100,9 @@ Section later.
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
-      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
+      split.
+      + intros Hxy [|n]; [done|apply Hxy].
+      + intros Hxy n; apply (Hxy (S n)).
     - split; rewrite /dist /later_dist.
       + by intros [x].
       + by intros [x] [y].

theories/algebra/sts.v

@@ -319,7 +319,9 @@ 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.
-  - intros. apply sts_frag_valid; split. by apply closed_up. set_solver.
+  - intros. apply sts_frag_valid; split.
+    + by apply closed_up.
+    + set_solver.
 Qed.
 
 Lemma sts_auth_frag_valid_inv s S T1 T2 :
@@ -377,8 +379,12 @@ Proof.
   rewrite /sts_frag=> HC HS HT. apply validity_update.
   inversion 3 as [|? S ? Tf|]; simplify_eq/=;
     (destruct HC as (? & ? & ?); first by destruct_and?).
-  - split_and!. done. set_solver. constructor; set_solver.
-  - split_and!. done. set_solver. constructor; set_solver.
+  - split_and!; first done.
+    + set_solver.
+    + constructor; set_solver.
+  - split_and!; first done.
+    + set_solver.
+    + constructor; set_solver.
 Qed.
 
 Lemma sts_update_frag_up s1 S2 T1 T2 :
@@ -393,7 +399,9 @@ Lemma sts_up_set_intersection S1 Sf Tf :
   closed Sf Tf → S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
 Proof.
   intros Hclf. apply (anti_symm (⊆)).
-  - move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
+  - move=>s [HS1 HSf]. split.
+    + by apply HS1.
+    + by apply subseteq_up_set.
   - move=>s [HS1 [s' [/elem_of_PropSet Hsup Hs']]]. split; first done.
     eapply closed_steps, Hsup; first done. set_solver +Hs'.
 Qed.

theories/algebra/updates.v

@@ -89,7 +89,9 @@ Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
 Proof.
   intros H n mz Hmz. apply H, Hmz.
   apply (cmra_validN_le n); last lia.
-  destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz.
+  destruct mz.
+  - eapply cmra_validN_op_l, Hmz.
+  - apply Hmz.
 Qed.
 
 (** ** Frame preserving updates for total CMRAs *)

theories/algebra/vector.v

@@ -27,7 +27,9 @@ Section ofe.
     Discrete x → Discrete v → Discrete (x ::: v).
   Proof.
     intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
-    constructor. by apply discrete. change (v ≡ v'). by apply discrete.
+    constructor.
+    - by apply discrete.
+    - change (v ≡ v'). by apply discrete.
   Qed.
   Global Instance vec_ofe_discrete m : OfeDiscrete A → OfeDiscrete (vecO m).
   Proof. intros ? v. induction v; apply _. Qed.

theories/base_logic/algebra.v

@@ -71,7 +71,9 @@ Section excl.
                         | _, _ => False
                         end.
   Proof.
-    uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
+    uPred.unseal. do 2 split.
+    - by destruct 1.
+    - by destruct x, y; try constructor.
   Qed.
   Lemma excl_validI x :
     ✓ x ⊣⊢@{uPredI M} if x is ExclBot then False else True.

theories/base_logic/derived.v

@@ -81,7 +81,7 @@ Qed.
 (** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
-Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
+Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 
 (** Consistency/soundness statement *)
 Lemma bupd_plain_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.