Commit 6784ac89 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix `iSimpl .. in ..`.

Thanks to @Blaisorblade for reporting.
parent 84444c51
Pipeline #13259 passed with stage
in 18 minutes and 48 seconds
......@@ -74,6 +74,17 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
--------------------------------------∗
▷^(S n + S m) emp
"test_iSimpl_in"
: string
1 subgoal
PROP : sbi
x, y : nat
============================
"H" : ⌜S (S (S x)) = y⌝
--------------------------------------∗
⌜S (S (S x)) = y⌝
"test_iFrame_later_1"
: string
1 subgoal
......
......@@ -412,6 +412,10 @@ Proof.
done.
Qed.
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.
Lemma test_iIntros_pure_neg : ( ¬False : PROP)%I.
Proof. by iIntros (?). Qed.
......
......@@ -119,8 +119,8 @@ Tactic Notation "iEval" tactic(t) "in" constr(H) :=
|pm_reflexivity
|].
Tactic Notation "iSimpl" := iEval simpl.
Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
Tactic Notation "iSimpl" := iEval (simpl).
Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
......
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