Commit 032879e0 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix some typos in comments.

parent b62bb39a
...@@ -691,8 +691,8 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := ...@@ -691,8 +691,8 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
|(* (?P -∗ _) *) eapply tac_wand_intro_pure; |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
[let P := match goal with |- IntoPure ?P _ => P end in [let P := match goal with |- IntoPure ?P _ => P end in
apply _ || fail "iIntro:" P "not pure"|] apply _ || fail "iIntro:" P "not pure"|]
|(* (■ ∀ _, _) *) apply tac_pure_forall_intro |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
|(* (■ (_ → _)) *) apply tac_pure_impl_intro]; |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
intros x. intros x.
Local Tactic Notation "iIntro" constr(H) := first Local Tactic Notation "iIntro" constr(H) := first
...@@ -1163,7 +1163,7 @@ Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) := ...@@ -1163,7 +1163,7 @@ Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
iRewriteCore true lem in H. iRewriteCore true lem in H.
Ltac iSimplifyEq := repeat ( 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/=). || simplify_eq/=).
(** * Update modality *) (** * Update modality *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment