The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Tue, Oct 26, 2010 at 01:36:53PM +0200, 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 ssreflect extension provides some facilities for this. See
<http://hal.inria.fr/docs/00/40/93/56/PDF/main.pdf>, Section 7.3.

Cheers,


Lauri