Spurious whitespace in proofmode notations
This is probably a result of !59 (merged). For example:
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
Coq now displays:
______________________________________(1/1)
"H3" : R
--------------------------------------□
"H1" : P
"H2" : Q
--------------------------------------∗
P ∗ Q
So, as you can see, the printing of each context starts with a spurious whitespace.
I don't know whether this is a Coq bug, or a bug in our notation. @jung any idea?