Weird automatically generated names
After @tchajed's !479 (merged) the following happens:
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
This names the automatically generated hypothesis x
.
1 subgoal
PROP : bi
x : True
______________________________________(1/1)
_ : ⌜0 = 0⌝
--------------------------------------□
True
I don't understand where the name x
comes from, but it's very annoying. The ∃ _ : ..., ...
pattern is often used for inG
, and the inG
being called x
is very annoying. It prevents one from using x
for other variables.
Obviously, in this case I could use iDestruct foo as (name_for_my_inG) "?"
, but I really don't want to name that hypothesis.