anomaly involving custom notations, grammar coercions, and ltac

[andres-erbsen]

Description of the problem

This can probably be minimized further

Notation ident_to_string x := ltac:(exact O).
Declare Custom Entry myident.
Notation "$ x" := x (in custom myident at level 0, x constr at level 0, format "'$' x").
Declare Custom Entry myexpr.
Notation "myexpr:( e )" := e (e custom myexpr, format "'myexpr:(' e ')'").
Notation "x" := x (in custom myexpr at level 0, x custom myident).
Notation "x" := (ident_to_string x) (in custom myexpr, x ident, only parsing).
Goal True.
  epose (myexpr:($1)).
 (* Anomaly "File "interp/constrintern.ml", line 994, characters 12-18: Assertion failed."
    Please report at http://coq.inria.fr/bugs/. *)

Coq Version

• master from yesterday, 65b2768
• 8.14.1

[SkySkimmer]

Duplicate #13966 ?

[SkySkimmer]

(which had to be re-fixed in #15343)

[herbelin]

Yes, this is prevented by #15343.

Maybe inclusion of entries (here of both myident and ident in myexpr) could also be more tolerant one day.