diff options
| author | Hugo Herbelin | 2015-01-24 21:48:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-24 22:27:57 +0100 |
| commit | bb37153d90de103dabd02285d11b3c39e3e4f89c (patch) | |
| tree | 293f7c5f30f4733982e55d4c8e13ef07c7222e94 | |
| parent | 0e06c54a9249477fdab5b135ffdac4bd3ea501a5 (diff) | |
Updating CHANGES (grammar, thanks to AS for pointing it out) +
a line on "Intuition Negation Unfolding".
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -120,7 +120,7 @@ Tactics * New tactics "revgoals", "cycle" and "swap" to reorder goals. * The semantics of recursive tactics (introduced with "Ltac t := ..." or "let rec t := ... in ...") changed slightly as t is now - applied to every goals, not each goal independently. In particular + applied to every goal, not each goal independently. In particular it may be applied when no goals are left. This may cause tactics such as "let rec t := constructor;t" to loop indefinitely. The simple fix is to rewrite the recursive calls as follows: @@ -163,7 +163,9 @@ Tactics opposite side, new tactic "dtauto" is able to destruct any record-like inductive types, superseding the old version of "tauto". - Similarly, "intuition" has been made more uniform and, where it now - fails, "dintuition" can be used. (possible source of incompatibilities) + fails, "dintuition" can be used (possible source of incompatibilities). +- New option "Unset Intuition Negation Unfolding" for deactivating automatic + unfolding of "not" in intuition. - Tactic notations can now be defined locally to a module (use "Local" prefix). - Tactic "red" now reduces head beta-iota redexes (potential source of rare incompatibilities). |