diff options
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -45,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 @@ -58,6 +68,8 @@ Vernacular Commands - 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. +- Added generic syntax for “attributes”, as in: + `#[local] Lemma foo : bar.` Coq binaries and process model |