Cyril Cohen (Nov 26 2020 at 13:50): Cyril Cohen (Nov 26 2020 at 13:50):At some point, I thought this long awaited feature had been implemented, but I cannot find it in the doc. Is it wishful thinking?
Enrico Tassi (Nov 26 2020 at 13:52):They are called "custom entries" (in the whole Coq sources, and "entry" is a "non terminal")
Enrico Tassi (Nov 26 2020 at 13:52):don't ask me why
Cyril Cohen (Nov 26 2020 at 13:52):thanks!
Last updated: Apr 19 2024 at 09:01 UTC