From 032879e0bdb9d51fa734706221aa8d925ee69494 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 27 Nov 2016 20:31:22 +0100
Subject: [PATCH] Fix some typos in comments.

---
 proofmode/tactics.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ce14c1f7d..ae871b950 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -691,8 +691,8 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
     |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
       [let P := match goal with |- IntoPure ?P _ => P end in
        apply _ || fail "iIntro:" P "not pure"|]
-    |(* (■ ∀ _, _) *) apply tac_pure_forall_intro
-    |(* (■ (_ → _)) *) apply tac_pure_impl_intro];
+    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
+    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
   intros x.
 
 Local Tactic Notation "iIntro" constr(H) := first
@@ -1163,7 +1163,7 @@ Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
   iRewriteCore true lem in H.
 
 Ltac iSimplifyEq := repeat (
-  iMatchGoal ltac:(fun H P => match P with (⌜_ = _⌝)%I => iDestruct H as %? end)
+  iMatchGoal ltac:(fun H P => match P with ⌜_ = _⌝%I => iDestruct H as %? end)
   || simplify_eq/=).
 
 (** * Update modality *)
-- 
GitLab