Commit 18f88572 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'isimpl_test' into 'master'

Add an `iSimpl in "%"` test.

See merge request iris/iris!240
parents 603bbea9 63adcecf
...@@ -122,6 +122,13 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi ...@@ -122,6 +122,13 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
--------------------------------------∗ --------------------------------------∗
⌜S (S (S x)) = y⌝ ⌜S (S (S x)) = y⌝
"test_iSimpl_in4"
: 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>",
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
"test_iFrame_later_1" "test_iFrame_later_1"
: string : string
1 subgoal 1 subgoal
......
...@@ -483,6 +483,10 @@ Lemma test_iSimpl_in3 x y z : ...@@ -483,6 +483,10 @@ Lemma test_iSimpl_in3 x y z :
S (S (S x)) = y : PROP. S (S (S x)) = y : PROP.
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed. Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
Check "test_iSimpl_in4".
Lemma test_iSimpl_in4 x y : (3 + x)%nat = y - S (S (S x)) = y : PROP.
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
Lemma test_iIntros_pure_neg : ( ¬False : PROP)%I. Lemma test_iIntros_pure_neg : ( ¬False : PROP)%I.
Proof. by iIntros (?). Qed. Proof. by iIntros (?). Qed.
......
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