From 32a12f974d29d11c4c010dbca92c02cba33ab716 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Mar 2018 17:33:33 +0100 Subject: Add some missing entries in CHANGES --- CHANGES | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 399e62de52..26f07540ad 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,11 @@ -Changes beyond 8.7 -================== +Changes from 8.7.2 to 8.8+beta1 +=============================== + +Kernel + +- Support for template polymorphism for definitions was removed. May trigger + more "universe inconsistency" errors in rare occasions. +- Fixpoints are no longer allowed on non-recursive inductive types. Notations @@ -56,6 +62,8 @@ Tactics - Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure properties of the executation of a tactic without keeping the effect of the execution. +- `vm_compute` now supports existential variables. +- Calls to `shelve` and `give_up` within calls to tactic `refine` now working. Focusing @@ -80,6 +88,9 @@ Vernacular Commands - The "Export" modifier can now be used when setting and unsetting options, and will result in performing the same change when the module corresponding the command is imported. +- The `Axiom` command does not automatically declare axioms as instances when + their type is a class. Previous behavior can be restored using `Set + Typeclasses Axioms Are Instances`. Universes @@ -106,6 +117,7 @@ Tools name scheme. This is intended to function as a linter for developments that want to be robust to changes in auto-generated names. This feature is experimental, and may change or dissapear without warning. +- GeoProof support was removed. Checker @@ -127,6 +139,9 @@ Documentation - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been moved to the GitHub wiki section of this repository; the main entry page is https://github.com/coq/coq/wiki/The-Coq-FAQ. +- Documentation: a large community effort resulted in the migration + of the reference manual to the Sphinx documentation tool. The result + is partially integrated in this version. Standard Library @@ -138,6 +153,7 @@ Standard Library positive, N, Z, and string. - Added [Coq.Strings.String.concat] to concatenate a list of strings inserting a separator between each item +- Notation `'` for Zpos in QArith was removed. - Some deprecated aliases are now emitting warnings when used. -- cgit v1.2.3 From 2c2e2af0659615c373aba8db82119e5eeba1bb49 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Mar 2018 17:34:48 +0100 Subject: Fix some items in Credits --- doc/sphinx/credits.rst | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index b4d816f9f3..ad7b8c4463 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1309,10 +1309,7 @@ with a few new features. The main user visible changes are: - Kernel: fix a subject reduction failure due to allowing fixpoints on non-recursive values, which allows to recover full parametricity for CIC, by Matthieu Sozeau. Handling of evars in the VM (the kernel - still does not accept evars) by Maxime Dénès. - -- Gallina: always use the projection printing style for primitive - projections by Maxime Dénès. + still does not accept evars) by Pierre-Marie Pédrot. - Notations: many improvements on recursive notations and integration with pattern binding by Hugo Herbelin. -- cgit v1.2.3 From fee3f7413a96a10ec2ac24f51b21d13a0838891f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 16 Mar 2018 10:10:33 -0300 Subject: Latest fixes. I think we can all agree this release has a chilean flavor anyway (as in hot and cold :) --- doc/sphinx/credits.rst | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index ad7b8c4463..a60f326454 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1311,8 +1311,8 @@ with a few new features. The main user visible changes are: for CIC, by Matthieu Sozeau. Handling of evars in the VM (the kernel still does not accept evars) by Pierre-Marie Pédrot. -- Notations: many improvements on recursive notations and - integration with pattern binding by Hugo Herbelin. +- Notations: many improvements on recursive notations and support for + destructuring patterns in the syntax of notations by Hugo Herbelin. - Proof language: tacticals for profiling, timing and checking success or failure of tactics by Jason Gross. The focusing bracket ``{`` @@ -1366,11 +1366,6 @@ The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www. -Packaging tools and software development kits were prepared by Michael -Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and -Maxime Dénès for macOS. Packages are regularly built on the -Travis and GitLab continuous integration server. - The 40 contributors for this version are Yves Bertot, Joachim Breitner, Tej Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle, Yannick Forster, Gaëtan Gilbert, Jason Gross, Samuel @@ -1401,6 +1396,6 @@ The |Coq| consortium, an organization directed towards users and supporters of the system, is now running and employs Maxime Dénès. The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. -| Paris, March 2018, -| Matthieu Sozeau and the |Coq| development team +| Santiago de Chile, March 2018, +| Matthieu Sozeau for the |Coq| development team | -- cgit v1.2.3