The Coq mailing list

[Maxime D�n�s <Maxime.Denes AT inria.fr>]

Dear Vladimir,

Boxed definitions were used to avoid early unfolding of constants by 
Coq's VM (if I remember correctly), and are now deprecated (I think 
these directives are interpreted as noop by the current trunk), hence 
probably the lack of documentation.

Hope it helps.

Maxime.

On 21/05/2011 20:09, Vladimir Voevodsky wrote:
> What does this command do? It is not in the command index of the reference 
> manual.
>
> Thanks!
> Vladimir.