diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 20 |
1 files changed, 19 insertions, 1 deletions
@@ -5,6 +5,8 @@ Tools - Coq_makefile lets one override or extend the following variables from the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS. + COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles + $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS). Vernacular Commands @@ -14,7 +16,8 @@ Vernacular Commands Tactic language - Support for fix/cofix added in Ltac "match" and "lazymatch". -- Ltac backtraces now contain include trace information about tactics + +- Ltac backtraces now include trace information about tactics called by OCaml-defined tactics. - Option "Ltac Debug" now applies also to terms built using Ltac functions. @@ -27,6 +30,18 @@ Tools Coq was ignoring previous runs and the -async-proofs-delegation-threshold option did not have the expected behavior. +Tactic language + +- The undocumented "nameless" forms `fix N`, `cofix N` have been + deprecated; please use `fix/cofix ident N` to explicitely name + hypothesis to be introduced. + +Documentation + +- The reference manual is now fully ported to Sphinx. + +Other small deprecations and bug fixes. + Changes from 8.7.2 to 8.8+beta1 =============================== @@ -93,6 +108,7 @@ Tactics of the execution. - `vm_compute` now supports existential variables. - Calls to `shelve` and `give_up` within calls to tactic `refine` now working. +- Deprecated tactic `appcontext` was removed. Focusing @@ -196,6 +212,7 @@ Options + `Refolding Reduction` + `Standard Proposition Elimination` + + `Dependent Propositions Elimination` + `Discriminate Introduction` + `Shrink Abstract` + `Tactic Pattern Unification` @@ -203,6 +220,7 @@ Options + `Injection L2R Pattern Order` + `Record Elimination Schemes` + `Match Strict` + + `Tactic Compat Context` + `Typeclasses Legacy Resolution` + `Typeclasses Module Eta` + `Typeclass Resolution After Apply` |