Commit d88d654b authored by Robbert Krebbers's avatar Robbert Krebbers

Adding `%I` to printing of proof mode hypotheses.

We already do the same for the goal, this avoids some scope
delimiters being displayed.
parent e2ece00a
Pipeline #9785 passed with stage
in 16 minutes
...@@ -75,6 +75,19 @@ Tactic failure: iFrame: cannot frame Q. ...@@ -75,6 +75,19 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗ --------------------------------------∗
□ P □ 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 1 subgoal
PROP : sbi PROP : sbi
......
...@@ -485,6 +485,12 @@ Proof. ...@@ -485,6 +485,12 @@ Proof.
iIntros "[??]". iSplit; last done. Show. done. iIntros "[??]". iSplit; last done. Show. done.
Qed. Qed.
Lemma test_big_sepL_simpl x (l : list nat) P :
P -
([ list] ky l, <affine> y = y ) -
([ list] y x :: l, <affine> y = y ) -
P.
Proof. iIntros "HP ?? /=". Show. done. Qed.
End tests. End tests.
(** Test specifically if certain things print correctly. *) (** Test specifically if certain things print correctly. *)
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
N : namespace N : namespace
P : iProp Σ P : iProp Σ
============================ ============================
"H" : inv N (<pers> P)%I "H" : inv N (<pers> P)
"H2" : ▷ <pers> P "H2" : ▷ <pers> P
--------------------------------------□ --------------------------------------□
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P) |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
...@@ -21,7 +21,7 @@ ...@@ -21,7 +21,7 @@
N : namespace N : namespace
P : iProp Σ P : iProp Σ
============================ ============================
"H" : inv N (<pers> P)%I "H" : inv N (<pers> P)
"H2" : ▷ <pers> P "H2" : ▷ <pers> P
--------------------------------------□ --------------------------------------□
"Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
...@@ -39,7 +39,7 @@ ...@@ -39,7 +39,7 @@
N : namespace N : namespace
P : iProp Σ P : iProp Σ
============================ ============================
_ : cinv N γ (<pers> P)%I _ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P "HP" : ▷ <pers> P
--------------------------------------□ --------------------------------------□
"Hown" : cinv_own γ p "Hown" : cinv_own γ p
...@@ -57,7 +57,7 @@ ...@@ -57,7 +57,7 @@
N : namespace N : namespace
P : iProp Σ P : iProp Σ
============================ ============================
_ : cinv N γ (<pers> P)%I _ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P "HP" : ▷ <pers> P
--------------------------------------□ --------------------------------------□
"Hown" : cinv_own γ p "Hown" : cinv_own γ p
...@@ -77,7 +77,7 @@ ...@@ -77,7 +77,7 @@
P : iProp Σ P : iProp Σ
H2 : ↑N ⊆ E2 H2 : ↑N ⊆ E2
============================ ============================
_ : na_inv t N (<pers> P)%I _ : na_inv t N (<pers> P)
"HP" : ▷ <pers> P "HP" : ▷ <pers> P
--------------------------------------□ --------------------------------------□
"Hown1" : na_own t E1 "Hown1" : na_own t E1
...@@ -98,7 +98,7 @@ ...@@ -98,7 +98,7 @@
P : iProp Σ P : iProp Σ
H2 : ↑N ⊆ E2 H2 : ↑N ⊆ E2
============================ ============================
_ : na_inv t N (<pers> P)%I _ : na_inv t N (<pers> P)
"HP" : ▷ <pers> P "HP" : ▷ <pers> P
--------------------------------------□ --------------------------------------□
"Hown1" : na_own t E1 "Hown1" : na_own t E1
......
...@@ -8,10 +8,10 @@ Arguments Enil {_}. ...@@ -8,10 +8,10 @@ Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%I. Arguments Esnoc {_} _%proof_scope _%string _%I.
Notation "" := Enil (only printing) : proof_scope. 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, (at level 1, P at level 200,
left associativity, format "Γ H : '[' P ']' '//'", only printing) : proof_scope. 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, (at level 1, P at level 200,
left associativity, format "Γ '_' : '[' P ']' '//'", only printing) : proof_scope. left associativity, format "Γ '_' : '[' P ']' '//'", only printing) : proof_scope.
......
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