From d88d654b8ba0301030a366ea6757da30ff5e3255 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Jun 2018 22:08:22 +0200
Subject: [PATCH] Adding `%I` to printing of proof mode hypotheses.

We already do the same for the goal, this avoids some scope
delimiters being displayed.
---
 tests/proofmode.ref           | 13 +++++++++++++
 tests/proofmode.v             |  6 ++++++
 tests/proofmode_iris.ref      | 12 ++++++------
 theories/proofmode/notation.v |  4 ++--
 4 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3460e251b..0ed7413b4 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -75,6 +75,19 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   â–¡ P
   
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  l : list nat
+  P : PROP
+  ============================
+  "HP" : P
+  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
+  _ : <affine> ⌜x = x⌝ ∗ ([∗ list] y ∈ l, <affine> ⌜y = y⌝)
+  --------------------------------------∗
+  P
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2359d047a..1931f99ed 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -485,6 +485,12 @@ Proof.
   iIntros "[??]". iSplit; last done. Show. done.
 Qed.
 
+Lemma test_big_sepL_simpl x (l : list nat) P :
+  P -∗
+  ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
+  ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
+  P.
+Proof. iIntros "HP ?? /=". Show. done. Qed.
 End tests.
 
 (** Test specifically if certain things print correctly. *)
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 317ac0b31..f2fe3bd8e 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -7,7 +7,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  "H" : inv N (<pers> P)%I
+  "H" : inv N (<pers> P)
   "H2" : â–· <pers> P
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
@@ -21,7 +21,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  "H" : inv N (<pers> P)%I
+  "H" : inv N (<pers> P)
   "H2" : â–· <pers> P
   --------------------------------------â–¡
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
@@ -39,7 +39,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  _ : cinv N γ (<pers> P)%I
+  _ : cinv N γ (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown" : cinv_own γ p
@@ -57,7 +57,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  _ : cinv N γ (<pers> P)%I
+  _ : cinv N γ (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown" : cinv_own γ p
@@ -77,7 +77,7 @@
   P : iProp Σ
   H2 : ↑N ⊆ E2
   ============================
-  _ : na_inv t N (<pers> P)%I
+  _ : na_inv t N (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown1" : na_own t E1
@@ -98,7 +98,7 @@
   P : iProp Σ
   H2 : ↑N ⊆ E2
   ============================
-  _ : na_inv t N (<pers> P)%I
+  _ : na_inv t N (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown1" : na_own t E1
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 33019f9c1..03fb2f02b 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -8,10 +8,10 @@ Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%I.
 
 Notation "" := Enil (only printing) : proof_scope.
-Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
+Notation "Γ H : P" := (Esnoc Γ (INamed H) P%I)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  '[' P ']' '//'", only printing) : proof_scope.
-Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
+Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P%I)
   (at level 1, P at level 200,
    left associativity, format "Γ '_'  :  '[' P ']' '//'", only printing) : proof_scope.
 
-- 
GitLab