Request for feedback on #14070 (token look-ahead in gramlib extended from sequential to tree-based)
Notes
Going ahead on #14070. Lifting this to backtrack across non-terminals seems non-trivial (and potentially problematic regarding performance)
We should add attributes to the available data in VERNAC EXTEND to choose the classifier.
Jim Fehrle needs some feedback on CoqIDE-related changes for the debugger.
Long discussion on modules/includes and locations of tactics. Jim will concentrate on a first solution that doesn't try to solve all
the corner cases.