The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

When you do "About blabla", you have all the informations about wich
argument in implicit or implicit and maximally inserted. So, just give
it a try ;)

Alexandre

2011/11/4 Victor Porton 
<porton AT narod.ru>:
> 04.11.2011, 06:53, "Brandon Moore" 
>Â <brandon_m_moore AT yahoo.com>:
>> The {...} binder is documented here
>> http://coq.inria.fr/refman/Reference-Manual004.html#htoc52
>> and the `(...) `{...} forms here
>> http://coq.inria.fr/refman/Reference-Manual004.html#htoc68
>>
>>> šAlso how to select when defining a type class between the four variants 
>>> or a
>>> šspecification of a class we build upon:
>>> š(...)
>>> š`(...)
>>> š{...}
>>> š`{...}
>>>
>>> šWhat are differences of these four variants?
>
> But what is the difference of `(...) and `{...}?
>
> --
> Victor Porton - http://portonvictor.org
>