The Coq mailing list

["Eduardo Gimenez" <Eduardo.Gimenez AT trusted-logic.fr>]

Try "Info Auto".

Cheers,
Eduardo.

----- Original Message -----
From: "Romain Janvier" 
<Romain.Janvier AT imag.fr>
To: 
<coq-club AT pauillac.inria.fr>
Sent: Wednesday, December 11, 2002 4:30 PM
Subject: [Coq-Club] How can I know what a tactic do in my proof?


> For example, if I make a proof using the tacic Auto, the proof will only
> be "Auto.".
> Is there a way to know what exacly as done the tactic: "Intros. Elim
H..."?
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>