The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Vladimir,

If you want to prove some properties but not name the properties you
can use "Goal" instead of "Lemma".

Randy


On Fri, Oct 24, 2014 at 6:47 AM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> Hello,
>
> is there a way to make sure that a certain identifier can not be used? The 
> closest that I know to it is to make an identifier opaque but
> I would like to make sure that an identifier is not used at all, e.g., I 
> would like to say
>
> Hide identity_ind.
>
> and then if a tactic wants to use it it will generate an error.
>
> Vladimir.
>
>
>