The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Thanks! I am trying to understand the standard library and it is full of 
commands which I never heard about.  Here is another question:

in [ Hint Unfold not: core. ] what does [ ... : core ] do ?? (I know that [ 
core ] is one of the three main notation scopes but [ not ] is not a notation 
.... )

Vladimir.







On May 21, 2011, at 2:12 PM, Maxime Dénès wrote:

> 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.