Polynomial : notation conflict concerning [[ and ]]

[letouzey]

As already mentioned in #46 I'm an happy user of QuantumLib, thanks a lot for this lib. Nonetheless there's a little detail that I find quite annoying. In QuantumLib.Polynomial, there is the following notation:

Notation "P [[ x ]]" := (Peval P x) (at level 0) : poly_scope.

The issue is that it currently breaks any nested use of other notations involving [ ].
For instance:

From Coq Require Import List.
From QuantumLib Require Import Polynomial.
Import ListNotations.
Check [ [O] ]. (* list (list nat) as expected, but only thanks to the spaces added between the square brackets *)
Check [[O]]. (* syntax error *)

Same (and more annoying actually) for nested patterns such as [[U|V]|W], also a syntax error as soon as Polynomial is Require'd, unless artificial blanks are added between consecutive square brackets.

Closing the poly_scope scope does not help (btw, could you please avoid this global open of poly_scope in Polynomial ?).

I suggest enclosing the notation for Peval in a little inner module, say PolyNotations (just like ListNotations ) to avoid forcing anyone to "benefit" unconditionally from this notation. Or find an alternative not based on square bracket maybe ?

Best regards
Pierre Letouzey, IRIF lab, Université Paris Cité