"Show Existentials" doesn't visually distinguish named goals from unnamed goals

[jfehrle]

Goal forall n m:nat, m > 0 -> True /\ False.
intros.
split.
2: refine ?[Goal].
Show Existentials.
  (*
  Existential 1 = ?Goal : [n : nat  m : nat  H : m > 0 |- True]      BOTH HAVE "?Goal"!
  Existential 2 = ?Goal : [n : nat  m : nat  H : m > 0 |- False]
  *)
[Goal] : shelve.
Show Existentials.
  (*  SHELVES THE NAMED GOAL (the one with False)
  Existential 1 = ?Goal : [n : nat  m : nat  H : m > 0 |- True]
  Existential 2 = ?Goal : [n : nat  m : nat  H : m > 0 |- False] (shelved)
  *)

Also, this fails:

Goal forall n m:nat, m > 0 -> True /\ False.
intros.
split.
Show Existentials.
  (*
  Existential 1 = ?Goal : [n : nat  m : nat  H : m > 0 |- True]
  Existential 2 = ?Goal0 : [n : nat  m : nat  H : m > 0 |- False]
  *)
[Goal] : shelve.
 (* Fails: No such goal. *)

[Zimmi48]

To your second point, that's not a bug, that's because goals that are not explicitly named cannot be referred using the printed named. Turning this into usability (which I think better reflect the issue that you are highlighting).

[SkySkimmer]

What would be a good way to print them? ?foo is the syntax to refer to named evar and should probably be reserved for those with real names. ?[foo] produces an evar with name foo and errors if the name is already used ?[?foo] produces an evar with a fresh name based on foo

I guess ?[?foo] could be OK? It doesn't feel great though.

[jfehrle]

The printed representation has to be parsable? Square brackets in Print Existentials make sense because that's how you create a named goal. ?[?foo] makes sense though it does look a little odd.