Ssreflect Users Discussion List

[Maxime Dénès <>]

Hi,

You can also pass "-w -notation-overriden,-deprecated" to coqc through
coq_makefile (using -arg) to silence those warnings.

Maxime.

On 12/21/16 20:11, Enrico Tassi wrote:
> On Wed, Dec 21, 2016 at 05:21:24PM +0000, Ilya Sergey wrote:
>> Hi Enrico,
>>
>> Thanks a lot for the update!
>>
>> One thing: at the moment math-comp, when building with the new Coq 8.6,
>> complains a lot about deprecated Vernacular commands, such as Arguments
>> Scope, as well about overloaded notations when importing ssrnat (e.g.,
>> *"**Warning:
>> Notation _ < _ <= _ was already used in scope nat_scope**"*).
>>
>> Is there an simple workaround to suppress them?
> 
> Unfortunately not.  We should really update the theory files...
> 
> Best,
>