tag name | V8.8.2 (eedbcabd26d0ee04c0ea9688e3bf0494bd534218) |
tag date | 2018-09-26 08:37:20 (GMT) |
tagged by | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> |
tagged object | commit 0ed45a5994... |
download | coq-8.8.2.zip coq-8.8.2.tar.gz coq-8.8.2.tar.bz2 |
---|
Version 8.8.2 of the Coq proof assistant.
Main changes:
- The kernel does not tolerate capture of global universes by
polymorphic universe binders, fixing a soundness break (triggered
only through custom plugins)
- A PDF version of the reference manual is available once again.
- The coq-makefile targets `print-pretty-timed`, `print-pretty-timed-diff`,
and `print-pretty-single-time-diff` now correctly label the "before" and
"after" columns, rather than swapping them.
- The Windows installer now includes many more external packages that can be
individually selected for installation.
Many other bug fixes and lots of documentation improvements (for details,
see the 8.8.2 milestone at https://github.com/coq/coq/milestone/15?closed=1).
-----BEGIN PGP SIGNATURE-----
iQIzBAABCAAdFiEEkKnyUFyKWZzTYN+P8XRKCUL1NscFAlurRegACgkQ8XRKCUL1
NsfumRAAmTD7gUttq86bg95OKG9VTpxLtmpAX/3H46EtA5EUeuryv4KgBpbLX3Eo
t/dwmrmemKn1r7Wk9TsHhlR1/iykPTv18F8fTF0w6Uarw7pHvMvtSrJgziqd3YrC
1Spm2pMDmrxjZNf4gObsAF7AFUhvKsKUeXxyXxATR32DlFcP+vi9boPzWKpLDVje
TVZ/KB8LjyygyV51MlE2mS4YxIOjrFvyOnpdQdMfRnAAAYCJPbSXbtKoEWoQ4LXp
ec6hH9tol4XYjK3+YUbxkaqf4iYCt7sUfYBFpJpXlBiHYa9EJvRx1RLZG0jLDZLK
8D3xQexfN5XEiqtv8d8n4rNn2NJR3dP5KvVAzgWLRFp/1V0ZfZyjMcuFFBIVKvmP
U3GJy5EbwSPegANHaqzY4/Kf0KRSHHMZkru0w6CiNeP7m6FuOLXzVfjLaNop76gO
oZtkoFXvWNiPUbl2mDIIpX3V0gvQscuvOhFcAMmVVc0yb40ut9i7lAsfnHDxKLKo
K3AaEqE/4aRdv43cZV3LDuycc100srBj4OmBg1agXb2KKLp6JXwQn0qAuOvZ9uQb
zSploZlmbWAYcL7AAeeijtp0d8Flrn5s4u1D4++TAe3/pZggWQIufGhFGVK5ZOdV
M+Ti9n2xwBUkpXdjzkMSyGXNZ8zxy3fAZDku+HcELhdV+cJAmK0=
=WQJh
-----END PGP SIGNATURE-----