incompleteness of Tauto about coq

[coqbot]

Full_Name: Laurent Gottely
Version: 7.0
OS: Linux
Submission from: machine107.cnet.fr (193.49.124.107)

Here are two examples of propositions which should be decided by Tauto (and
which used to be decided by Tauto in Coq V6.3.1):

Lemma bug_tauto : (A,B:Prop)((A->B->False)->False) -> (B->False) -> False.
Tauto.
=> Tauto failed.

Lemma bug_tauto_2 : (A,B,C:Prop)
((((C->False)->A)->((B->False)->A)->False)->False) ->
(((C->B->False)->False)->False) ->
~A->A.
Tauto.
=> Tauto failed.

[coqbot]

delahaye@ jurancon.inria.fr (David Delahaye)

Here are two examples of propositions which should be decided by Tauto (and
which used to be decided by Tauto in Coq V6.3.1):

This bug has been fixed (actually, the two bugs were due to the same

problem). Thank you for your report.

David.

===============================================================================
David Delahaye : David.Delahaye@ inria.fr
: The Coq Project : Proofs
: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
FRANCE
: (33)-(0)1 39 63 57 53
: (33)-(0)1 39 63 56 84
: http://pauillac.inria.fr/~delahaye

[Computers are like air conditioners - they stop working properly when you open
Windows.]

[coqbot]

Problem fixed by another bug fix