On 29/11/2018 14.11, Emilio Jesús Gallego Arias wrote: > Clément Pit-Claudel <clement....@gmail.com> writes: >>> Note even for the mainline, coqtop-based branch, many hacks in the code >>> could be removed today if so we wished. >> >> I'm not sure I understand this part > > See for example: > > - https://github.com/coq/coq/issues/7591 > - https://github.com/ProofGeneral/PG/issues/212 > > Among others, that would allow to drop all the code manipulating `Set > Silent`, having to parse documents, etc...
Ah, yes, of course; but removing that code requires dropping support for old versions of Coq.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
