The Coq mailing list

[Matt Ridsdale <matt.ridsdale AT cl.cam.ac.uk>]

Oops! that'll teach me to check these things more carefully...

thanks


Adam Chlipala-3 wrote:
> 
> Matt Ridsdale wrote:
>> Lemma z_plus_commmutes : forall y : mynat, myplus Q y = myplus y Q.
>> [snip]
>> Check z_plus_commutes.
>>   
> 
> You are checking the wrong lemma name.
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.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
> 
> 

-- 
View this message in context: 
http://www.nabble.com/Check-lemma_name-gives-error-immediately-after-lemma-is-proved-tp21900669p21900767.html
Sent from the Coq mailing list archive at Nabble.com.