The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

I believe that ": core" means "in the core hint database.

On Sat, May 21, 2011 at 11:31 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

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.

-- 
gregory malecha