Notation clash between Sniper and Mathcomp's ssrnotations module

anton-trunov commented 3 years ago

From mathcomp Require Import ssrfun.
From Sniper Require Import Sniper.

produces the following error:

Error: Notation "_ .[ _ ]" is already defined at level 2 with arguments constr
at level 2, constr while it is now required to be at level 50 with arguments constr
at next level, constr.

This is because Mathcomp's ssrfun exports the ssrnotations module. Note that Coq's own ssrfun module does not have this notation clash.

Perhaps, Sniper's notations could be hidden behind a module, like ListNotations in Coq's stdlib? Or is it exported from somewhere else?

vblot commented 3 years ago

Thanks for this bug report. The bug was actually part of SMTCoq, and has been fixed in https://github.com/smtcoq/smtcoq/commit/01431eb67ed566baa2268f1382d687bc7b020d1c

anton-trunov commented 3 years ago

Thank you for taking care of this!

smtcoq / sniper

Notation clash between Sniper and Mathcomp's ssrnotations module #5