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
thanks!
Last updated: Oct 13 2024 at 01:02 UTC