From 191a6f43712ebca172e2e0a8bfc9eb643487453e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 28 Jun 2018 16:36:42 +0200
Subject: [PATCH] fix nits

---
 tests/proofmode.v        | 17 ++++++++---------
 theories/bi/telescopes.v | 10 +++++-----
 2 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9b57025be..d2ba302b5 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -534,15 +534,14 @@ Proof.
 Qed.
 
 Section wandM.
-Import proofmode.base.
-Lemma test_wandM mP Q R :
-  (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
-Proof.
-  iIntros "HPQ HQR HP". Show.
-  iApply "HQR". iApply "HPQ". Show.
-  done.
-Qed.
-
+  Import proofmode.base.
+  Lemma test_wandM mP Q R :
+    (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
+  Proof.
+    iIntros "HPQ HQR HP". Show.
+    iApply "HQR". iApply "HPQ". Show.
+    done.
+  Qed.
 End wandM.
 
 End tests.
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index 554cd0b27..d54533929 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -23,8 +23,8 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
 Section telescope_quantifiers.
   Context {PROP : bi} {TT : tele}.
 
-  Lemma bi_tforall_forall (Ψ : TT -> PROP) :
-    (bi_tforall Ψ) ⊣⊢ (bi_forall Ψ).
+  Lemma bi_tforall_forall (Ψ : TT → PROP) :
+    bi_tforall Ψ ⊣⊢ bi_forall Ψ.
   Proof.
     symmetry. unfold bi_tforall. induction TT as [|X ft IH].
     - simpl. apply (anti_symm _).
@@ -36,11 +36,11 @@ Section telescope_quantifiers.
         by rewrite (forall_elim (TargS a p)).
       + move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
         setoid_rewrite <- IH.
-        do 2 rewrite forall_elim. done.
+        rewrite 2!forall_elim. done.
   Qed.
 
-  Lemma bi_texist_exist (Ψ : TT -> PROP) :
-    (bi_texist Ψ) ⊣⊢ (bi_exist Ψ).
+  Lemma bi_texist_exist (Ψ : TT → PROP) :
+    bi_texist Ψ ⊣⊢ bi_exist Ψ.
   Proof.
     symmetry. unfold bi_texist. induction TT as [|X ft IH].
     - simpl. apply (anti_symm _).
-- 
GitLab