diff options
| author | letouzey | 2012-05-15 18:08:25 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-15 18:08:25 +0000 |
| commit | c5e6d03b4dc5a5f4dc2037fa19cb5f319aafb188 (patch) | |
| tree | 5784976f5771422c2559b023b812cfe16d3a1a89 /CHANGES | |
| parent | 1b5ab3052cd265dd6c7aafa100607c69b2693c29 (diff) | |
Intuition: temporary(?) restore the unconditional unfolding of not
Let's check tomorrow the impact on contribs: are the recent build
failures related to the "not" unfolding stategy or to the new
handling of conjonction-like constructors ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 1 insertions, 3 deletions
@@ -48,9 +48,7 @@ Tactics 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. Moreover, both of them are now only - lazily unfolding the occurrences of "not" in goal. Some extra - "unfold not in *" might have to be added for compatibility. + fails, "dintuition" can be used. - Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy) have been removed, since Why2 has not been maintained for the last few years. The Why3 plugin should be a suitable |