Verified Commit e47c73d8 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Fix parsing precedence for iEval

parent 8f443ec0
......@@ -126,7 +126,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
: string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
......@@ -480,6 +480,13 @@ Proof.
Lemma test_iEval_precedence : True True : PROP.
(* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
iEval (rewrite /=); iPureIntro; exact I.
Check "test_iSimpl_in".
Lemma test_iSimpl_in x y : (3 + x)%nat = y - S (S (S x)) = y : PROP.
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
......@@ -195,7 +195,7 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
iClear Hs; clear xs.
(** ** Simplification *)
Tactic Notation "iEval" tactic(t) :=
Tactic Notation "iEval" tactic3(t) :=
eapply tac_eval;
[let x := fresh in intros x; t; unfold x; reflexivity
......@@ -212,7 +212,7 @@ Local Ltac iEval_go t Hs :=
|pm_reduce; iEval_go t Hs]
Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
Tactic Notation "iSimpl" := iEval (simpl).
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