constr in Custom Entry mistaken for SELF

[Janno]

Description of the problem

The custom entry below treats parts p and b as custom expr instead of the specified constr.

Declare Custom Entry expr. Declare Custom Entry aux.
Notation "p u b" := (p (fun _ => b) u)
  (in custom expr at level 201, p constr, b constr, u custom aux at level 1).
Print Custom Grammar expr.
(*
Entry constr:expr is
[ "201" RIGHTA
  [ SELF; constr:aux LEVEL "1"; NEXT ] ]
*)

I suspect that this breaks some uses of my (more complicated) notations.

Coq Version

master, 8.10.2

[Janno]

It has to do with specifying the notation's level:

Declare Custom Entry expr.
Notation "{ p }" := (p)
  (in custom expr at level 201, p constr).
Notation "{ p }" := (p)
  (in custom expr, p constr).

The second notation correctly treats p as a constr whereas the first one doesn't.

[ppedrot]

The issue arises in Egramcoq.symbol_of_target. The from argument should also provide the ambient custom entry to be able to discriminate it against the entry being resolved. While this alone is easy to do, I don't really understand what adjust_level should do in that case, so I am deferring to @herbelin.

[herbelin]

See #11355 #11530 for a fix. Printing of custom entries was missing some polishing. Thanks a lot for reporting.