The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.