The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 07/07/2010 08:51, Pierre-Marie Pédrot a écrit :
> Have a semi-transparent flag stating that this term is transparent for
> reduction but not for unfolding in proofs (I don't think this is possible).

You can try using the "Strategy" command...

> [...] Actually, the more I use the module
> system, the more I find it useless because while providing a VITAL way
> to abstract things, it does conflict with a lot of other parts of Coq.

Indeed...


Best regards,

-- 
Stéphane