The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I don't think there is. What sort of use-case do you have in mind?

On 24 October 2014 12:47, 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.