From 63adcecfc45f9b56f71f0c19796c666d8997f935 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 6 May 2019 15:27:31 +0200
Subject: [PATCH] Add an `iSimpl in "%"` test.

---
 tests/proofmode.ref | 7 +++++++
 tests/proofmode.v   | 4 ++++
 2 files changed, 11 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 1004ce814..fb9e3a872 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -122,6 +122,13 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ⌜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"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 528eec38e..1e5d334cf 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -483,6 +483,10 @@ Lemma test_iSimpl_in3 x y z :
   ⌜ S (S (S x)) = y ⌝ : PROP.
 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.
 Proof. by iIntros (?). Qed.
 
-- 
GitLab