From e1f5180e88bf02a22c954ddbdcbdfeb168d264a6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Apr 2012 22:06:11 +0000
Subject: Fixing tauto "special" behavior on singleton types w/ 2 parameters
 (bug #2680). - tauto/intuition now works uniformly on and, prod, or, sum,
 False,   Empty_set, unit, True (and isomorphic copies of them), iff, ->, and 
  on all inhabited singleton types with a no-arguments constructor   such as
 "eq t t" (even though the last case goes out of   propositional logic: this
 features is so often used that it is   difficult to come back on it). - New
 dtauto and dintuition works on all inductive types with one   constructors
 and no real arguments (for instance, they work on   records such as
 "Equivalence"), in addition to -> and eq-like types. - Moreover, both of them
 no longer unfold inner negations (this is a   souce of incompatibility for
 intuition and evaluation of the level   of incompatibility on contribs still
 needs to be done).

Incidentally, and amazingly, fixing bug #2680 made that constants
InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto
had indeed destructed a section hypothesis "@StrictOrder A ltA@
thinking it was a conjunction, making this section hypothesis
artificially necessary while it was not.

Renouncing to the unfolding of inner negations made auto/eauto
sometimes succeeding more, sometimes succeeding less. There is by the
way a (standard) problem with not in auto/eauto: even when given as an
"unfold hint", it works only in goals, not in hypotheses, so that auto
is not able to solve something like "forall P, (forall x, ~ P x) -> P
0 -> False". Should we automatically add a lemma of type "HYPS -> A ->
False" in the hint database everytime a lemma ""HYPS -> ~A" is
declared (and "unfold not" is a hint), and similarly for all unfold
hints?

At this occasion, also re-did some proofs of Znumtheory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 91501ebcd9..cc365dce9f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -41,6 +41,16 @@ Tactics
   "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
 - New command "r string" that interprets "idtac string" as a breakpoint
   and jumps to its next use in Ltac debugger.
+- Tactic "tauto" was exceptionally able to destruct other connectives
+  than the binary connectives "and", "or", "prod", "sum", "iff".  This
+  non-uniform behavior has been fixed (bug #2680) and tauto is
+  slightly weaker. On the 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. 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.
 
 Libraries
 
-- 
cgit v1.2.3