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

1 files changed, 4 insertions, 4 deletions

diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 82e9e3b8e..e4ae55409 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -53,13 +53,13 @@ val is_non_recursive_type         : testing_function
 
 (** Non recursive type with no indices and exactly one argument for each
    constructor; canonical definition of n-ary disjunction if strict *)
-val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function
-val is_disjunction         : ?strict:bool -> testing_function
+val match_with_disjunction : ?strict:bool -> ?onlybinary:bool -> (constr * constr list) matching_function
+val is_disjunction         : ?strict:bool -> ?onlybinary:bool -> testing_function
 
 (** Non recursive tuple (one constructor and no indices) with no inner
    dependencies; canonical definition of n-ary conjunction if strict *)
-val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
-val is_conjunction         : ?strict:bool -> testing_function
+val match_with_conjunction : ?strict:bool -> ?onlybinary:bool -> (constr * constr list) matching_function
+val is_conjunction         : ?strict:bool -> ?onlybinary:bool -> testing_function
 
 (** Non recursive tuple, possibly with inner dependencies *)
 val match_with_record      : (constr * constr list) matching_function