Clément Pit-Claudel <clement....@gmail.com> writes: > Ah, yes, of course; but removing that code requires dropping support > for old versions of Coq.
I guess at some point it would make sense to tie PG to an specific Coq range; I think the required changes could be made in the range of Coq >= 8.8. Of course it would depend on how much the maintainers think it is worth it. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel