The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Like others, I do not really see the point of such a feature. But maybe 
the following suffices for your particular example:

(* Disable generation of eliminators *)
Unset Elimination Schemes.

(* Redefine identity yourself. No eliminators will be generated *)
Inductive identity (A : Type) (a : A) : A -> Type :=
  identity_refl : identity A a a.

If it is about "restricting" the use of an inductive type, you may want 
to look at Yves Bertot's private types.

On 10/24/2014 06:47 AM, Vladimir Voevodsky 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.