I'm making decent progress on getting PG to work with the Coq
The main stumbling block I'm having is making sure the spans have
the correct structure. Those are implemented by Emacs overlays.
Can someone explain what the structure of the spans should be, and
what metadata they should contain? Are there invariants that should
hold as a user steps through a proof?
I'm told that CoqIDE has a similar notion, but there's just one span
per sentence in a script. I'm noticing multiple, overlapping spans in
Currently, PG has machinery to know where a proof begins. If you
undo just past a finished proof, the entire proof is retracted. I'm
told that since 8.5, you can backtrack to the middle of a proof, so
that machinery is unneeded.
ProofGeneral-devel mailing list