custom entry printed as constr when global coercion is present

[andres-erbsen]

Description of the problem

Declare Custom Entry ent.
Notation "ent:( c )" := c (c custom ent).

Module One.
  Notation "x =" := (Some x) (in custom ent, x global).
  Check Some (1+2). (* ent:(1 + 2 =) *)
End One.

Module Both.
  Notation "$ x =" := (Some x) (in custom ent at level 0, x constr at level 0).
  Check ent:($(1+2) = ). (* ent:($ (1 + 2) =)  *) (* this one is fine *)
  Notation "x =" := (Some x) (in custom ent, x global).
  Check ent:($(1+2) = ). (* ent:(1 + 2 =) *)
End Both.

The last example in each module cannot be parsed back and I think should not be printed this way because 1+2 is not a global reference.

I wonder whether the issue might not be specific to global, but name didn't make this example print badly.

Note: we are using global there to fill in for wishes #9516 and #9518.

Coq Version

• 8.14.1
• master from yesterday, 65b2768

[samuelgruetter]

I ran into this (or a similar) issue, but without custom entries, so maybe the problem is not related to custom entries, but only to global?

Axiom foo: nat -> nat.

Notation "` x" := (foo x) (at level 9, x global, format "` x").

Check (fun a: nat => `a).
(* Prints "fun a : nat => `a" (ok) *)
Check (fun a => foo (a + a)).
(* Prints "fun a : nat => `a + a" (bad), should print "fun a => foo (a + a)" *)

Like in @andres-erbsen's example, if I replace global by name, it works as expected.