diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 38 |
1 files changed, 33 insertions, 5 deletions
@@ -5,6 +5,39 @@ Vernacular commands - New command "Redirect" to redirect the output of a command to a file. +Tactics + +- New flag "Regular Subst Tactic" which fixes "subst" in situations where + it failed to substitute all substitutable equations or failed to simplify + cycles, or accidentally unfolded local definitions (flag is off by default). +- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a + special way. It accepts three distinct flags: + * "Lax", which is the default one, sets the old behavior, i.e. a non-imported + hint behaves the same as an imported one. + * "Warn" outputs a warning when a non-imported hint is used. Note that this is + an over-approximation, because a hint may be triggered by an eauto run that + will eventually fail and backtrack. + * "Strict" changes the behavior of an unloaded hint to the one of the fail + tactic, allowing to emulate the hopefully future import-scoped hint mechanism. + +API + +- Some functions from pretyping/typing.ml and their derivatives were potential + source of evarmap leaks, as they dropped their resulting evarmap. The + situation was clarified by renaming them according to a unsafe_* scheme. Their + sound variant is likewise renamed to their old name. The following renamings + were made. + * Typing.type_of -> unsafe_type_of + * Typing.e_type_of -> type_of + * A new e_type_of function that matches the e_ prefix policy + * Tacmach.pf_type_of -> pf_unsafe_type_of + * A new safe pf_type_of function. + All uses of unsafe_* functions should be eventually eliminated. + + +Tools + +- Added an option -w to control the output of coqtop warnings. Changes from V8.5beta1 to V8.5beta2 =================================== @@ -19,7 +52,6 @@ Tactics - A script using the admit tactic can no longer be concluded by either Qed or Defined. In the first case, Admitted can be used instead. In the second case, a subproof should be used. - - The easy tactic and the now tactical now have a more predictable behavior, but they might now discharge some previously unsolved goals. @@ -27,25 +59,21 @@ Extraction - Definitions extracted to Haskell GHC should no longer randomly segfault when some Coq types cannot be represented by Haskell types. - - Definitions can now be extracted to Json for post-processing. Tools - Option -I -as has been removed, and option -R -as has been deprecated. In both cases, option -R can be used instead. - - coq_makefile now generates double-colon rules for rules such as clean. API - The interface of [change] has changed to take a [change_arg], which can be built from a [constr] using [make_change_arg]. - - [pattern_of_constr] now returns a triplet including the cleaned-up [evar_map], removing the evars that were turned into metas. - Changes from V8.4 to V8.5beta1 ============================== |