The Coq mailing list

["Pierre Cast�ran" <pierre.casteran AT labri.fr>]

Quoting "Adam Chlipala" 
<adamc AT hcoop.net>:


> P.S.: Please don't include long proof interaction traces in future  
> messages.  Showing one proof sequent would be enough for me, and I  
> almost ignored your message because of how long it was.  (Others may  
> have different opinions, but I'm guessing that most agree on this.)

Perhaps attaching a *small self contained*  .v file would allow us to
look quickly at the interactions under coqide or PFG, and try some  
modifications ...


Pierre
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/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



Pierre Castéran