At some point, I thought this long awaited feature had been implemented, but I cannot find it in the doc. Is it wishful thinking?
They are called "custom entries" (in the whole Coq sources, and "entry" is a "non terminal")
don't ask me why
Last updated: Jan 29 2023 at 01:02 UTC