ejgallego on master
Fixes #11254 (not requiring coq… Merge PR #11255: Fix #11254: "c… (compare)
@ppedrot that sounds a bit strange; indeed the thing with CEPs is that they are almost always very under-specified. Designing a document manager with holes doesn't seem trivial [and I've been doing that like 2 years, mostly on dedukti]
I'd start by adding such table on the record in
VernacState, there is no reason such state has to be like imperative.
Vernacstateand the one that can be smart here.