diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 53 |
1 files changed, 53 insertions, 0 deletions
@@ -1,6 +1,10 @@ Changes from 8.8.2 to 8.9+beta1 =============================== +Kernel + +- Mutually defined records are now supported. + Tactics - Added toplevel goal selector ! which expects a single focused goal. @@ -41,6 +45,16 @@ Tools COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS). +- Removed the gallina utility (extracts specification from Coq vernacular files). + If you would like to maintain this tool externally, please contact us. + +- Removed the Emacs modes distributed with Coq. You are advised to + use Proof-General <https://proofgeneral.github.io/> (and optionally + Company-Coq <https://github.com/cpitclaudel/company-coq>) instead. + If your use case is not covered by these alternative Emacs modes, + please open an issue. We can help set up external maintenance as part + of Proof-General, or independently as part of coq-community. + Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments @@ -48,6 +62,12 @@ Vernacular Commands - Nested proofs may be enabled through the option `Nested Proofs Allowed`. By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. +- Added option Uniform Inductive Parameters which abstracts over parameters + before typechecking constructors, allowing to write for example + `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` +- New Set Hint Variables/Constants Opaque/Transparent commands for setting + globally the opacity flag of variables and constants in hint databases, + overwritting the opacity set of the hint database. Coq binaries and process model @@ -61,19 +81,52 @@ Coq binaries and process model `coq{proof,tactic,query}worker` are in charge of task-specific and parallel proof checking. +SSReflect + +- The implementation of delayed clear switches in intro patterns + is now simpler to explain: + 1. The immediate effect of a clear switch like {x} is to rename the + variable x to _x_ (i.e. a reserved identifier that cannot be mentioned + explicitly) + 2. The delayed effect of {x} is that _x_ is cleared at the end of the intro + pattern + 3. A clear switch immediately before a view application like {x}/v is + translated to /v{x}. + In particular rule 3 lets one write {x}/v even if v uses the variable x: + indeed the view is executed before the renaming. + +- An empty clear switch is now accepted in intro patterns before a + view application whenever the view is a variable. + One can now write {}/v to mean {v}/v. Remark that {}/x is very similar + to the idiom {}e for the rewrite tactic (the equation e is used for + rewriting and then discarded). + Changes from 8.8.0 to 8.8.1 =========================== Kernel - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). +- Fix a critical bug with modules and algebraic universes (#7695) - Fix a critical bug with inlining of polymorphic constants (#7615). +- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was + present since 8.5. Notations - Fixed unexpected collision between only-parsing and only-printing notations (issue #7462). +Windows installer + +- The Windows installer now includes external packages Ltac2 and Equations + (it included the Bignums package since 8.8+beta1). + +Many other bug fixes, documentation improvements (including fixes of +regressions due to the Sphinx migration), and user message improvements +(for details, see the 8.8.1 milestone at +https://github.com/coq/coq/milestone/13?closed=1). + Changes from 8.8+beta1 to 8.8.0 =============================== |