The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

2011/11/8 Victor Porton 
<porton AT narod.ru>:
> But how to make it to work as intended, that is how to deal with the 
> projector "num" OF THE CURRENT INSTANCE INSIDE AN INSTANCE PROOF?

IT HAS ALREADY BEEN REPLACED BY ITS DEFINITION, WHICH IS WHY YOU HAVE
TO PROVE 0=0.


> Instance C2: C := { num:=0 }.
> proof.
> šhave (num=0) using tauto.
> end proof.

num is a projector, that expects an instance of the class C as an
argument, and you have not defined sur an instance yet. So your code
still makes *no sense*