From c6ea4aa9a48a10e796a99a00170377e0a8030868 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 4 Nov 2020 11:14:52 -0600
Subject: [PATCH] more feedback

---
 theories/algebra/cmra.v    |  8 +++++++-
 theories/algebra/sts.v     |  2 +-
 theories/si_logic/bi.v     |  8 ++++++--
 theories/si_logic/siprop.v | 13 +++++++++++--
 4 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 4a7325f8b..cfc26604a 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -747,7 +747,13 @@ End cmra_total.
 
 (** * Properties about morphisms *)
 Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
-Proof. split=>//=; first apply _. intros. by rewrite option_fmap_id. Qed.
+Proof.
+  split => /=.
+  - apply _.
+  - done.
+  - intros. by rewrite option_fmap_id.
+  - done.
+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) :
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 9a1d784b1..fae53edbd 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -321,7 +321,7 @@ Proof.
   - move=>/sts_frag_valid [H _]. apply H, elem_of_up.
   - intros. apply sts_frag_valid; split.
     + by apply closed_up.
-    + set_solver.
+    + set_solver+.
 Qed.
 
 Lemma sts_auth_frag_valid_inv s S T1 T2 :
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 4d66d06d6..6dbcd41a3 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -97,11 +97,15 @@ Proof.
   - exact: @later_exist_false.
   - (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
     intros P Q.
-    apply and_intro; apply later_mono; [ apply and_elim_l | apply and_elim_r ].
+    apply and_intro; apply later_mono.
+    + apply and_elim_l.
+    + apply and_elim_r.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q.
     trans (siProp_forall (λ b : bool, siProp_later (if b then P else Q))).
-    { apply forall_intro=> -[]; [ apply and_elim_l | apply and_elim_r ]. }
+    { apply forall_intro=> -[].
+      - apply and_elim_l.
+      - apply and_elim_r. }
     etrans; [apply later_forall_2|apply later_mono].
     apply and_intro.
     + refine (forall_elim true).
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 977c52f86..30343ff49 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -215,14 +215,23 @@ Proof. unseal; by split=> n [??]. Qed.
 Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
 Proof. unseal; by split=> n [??]. Qed.
 Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
-Proof. intros HQ HR; unseal; split=> n ?; by split; [apply HQ|apply HR]. Qed.
+Proof.
+  intros HQ HR; unseal; split=> n ?.
+  split.
+  - by apply HQ.
+  - by apply HR.
+Qed.
 
 Lemma or_intro_l P Q : P ⊢ P ∨ Q.
 Proof. unseal; split=> n ?; left; auto. Qed.
 Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
 Proof. unseal; split=> n ?; right; auto. Qed.
 Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof. intros HP HQ. unseal; split=> n [?|?]; [by apply HP | by apply HQ]. Qed.
+Proof.
+  intros HP HQ. unseal; split=> n [?|?].
+  - by apply HP.
+  - by apply HQ.
+Qed.
 
 Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
 Proof.
-- 
GitLab