The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

[To: 
coq-club AT pauillac.inria.fr]

I'm in the middle of a big long proof, and for some strange reason I got
to a point where the Assumption tactic seems to hang the system.

I don't really want to see if this bug exists in 7.3 since last time I
tried to move to 7.3 I found that the Tauto tactic behaved differently,
and I didn't feel like reworking my proof.

I don't know if it is worth reporting this bug since I have no idea what I
did to make it happen, and it hardly seems worth providing my big library
to track this down.

Is this a known problem in 7.2?

- -- 
Russell O'Connor            <http://www.math.berkeley.edu/~roconnor/>
``[Law enforcement officials] suggested that the activists were stopped
not because their names are on the list, but because their names resemble
those of suspected criminals or terrorists.'' -- SFGate.com
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.0.6 (SunOS)
Comment: For info see http://www.gnupg.org

iD8DBQE9yGLUuZUa0PWVyWQRAm02AJ9/nlDBo+9QWOee8QhDCsvOOGaOhwCfSus2
yFBc6h631uUB2HFJXVexfe4=
=g+ZY
-----END PGP SIGNATURE-----