diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 36 |
1 files changed, 35 insertions, 1 deletions
@@ -6,6 +6,9 @@ Tactics - New tactic "extensionality in H" which applies (possibly dependent) functional extensionality in H supposed to be a quantified equality until giving a bare equality. +- Tactic "specialize with ..." now accepts any partial bindings. + Missing bindings are either solved by unification or left quantified + in the hypothesis. - New representation of terms that statically ensure stability by evar-expansion. This has several consequences. * In terms of performance, this adds a cost to every term destructuration, @@ -17,12 +20,27 @@ Tactics Most notably, the new implementation recognizes Miller patterns that were missed before because of a missing normalization step. Hopefully this should be fairly uncommon. -- "auto with real" can now discharge comparisons of literals +- Tactic "auto with real" can now discharge comparisons of literals. - The types of variables in patterns of "match" are now beta-iota-reduced after type-checking. This has an impact on the type of the variables that the tactic "refine" introduces in the context, producing types a priori closer to the expectations. +- In "Tactic Notation" or "TACTIC EXTEND", entry "constr_with_bindings" + now uses type classes and rejects terms with unresolved holes, like + entry "constr" does. To get the former behavior use + "open_constr_with_bindings" (possible source of incompatibility. +- New e-variants eassert, eenough, epose proof, eset, eremember, epose + which behave like the corresponding variants with no "e" but turn + unresolved implicit arguments into existential variables, on the + shelf, rather than failing. +Vernacular Commands + +- Goals context can be printed in a more compact way when "Set + Printing Compact Contexts" is activated. + +- The deprecated `Save` vernacular and its form `Save Theorem id` to + close proofs have been removed from the syntax. Please use `Qed`. Standard Library @@ -47,6 +65,22 @@ Dependencies - Support for camlp4 has been removed. +Tools + +- coq_makefile was completely redesigned to improve its maintainability and + the extensibility of generated Makefiles, and to make _CoqProject files + more palatable to IDEs. Overview: + * _CoqProject files contain only Coq specific data (i.e. the list of + files, -R options, ...) + * coq_makefile translates _CoqProject to Makefile.conf and copies in the + desired location a standard Makefile (that reads Makefile.conf) + * Makefile extensions can be implemented in a Makefile.local file (read + by the main Makefile) by installing a hook in the extension points + provided by the standard Makefile + The current version contains code for retro compatibility that prints + warnings when a deprecated feature is used. Please upgrade your _CoqProject + accordingly. + Changes from V8.6beta1 to V8.6 ============================== |