The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Alexandre Pilkiewicz wrote:
> I would like to declare some definitions to be not unfoldable by
> simpl, so that it doesn't go "too far".
> I tried "Opaque myconst.", but then, even unfold fails.
>
> I there a better way?
>    

The only way I've found to do this is to put the definition inside a 
module with opaque signature ascription.  You can also export from the 
module a theorem giving the equation defining the identifier; then, in 
cases where you do want reduction, you have to rewrite with that 
equality, rather than relying on the definitional equality.