Notations conflict with stdlib.

[nrioux]

My AS2-generated file contains the line:

Notation "[ sigmaval ]" := (subst_tm sigmaval) (at level 1, left associativity, only printing) : fscope.

Unfortunately, this notation conflicts with the definition from Coq.Lists.List.ListNotations:

Notation "[ x ]" := (cons x nil) : list_scope.

As a result, given an AS2-generated module syntax, the following code

Require Import Coq.Lists.List.
Import ListNotations.
Require Import syntax.

produces the error

Error: Notation "[ _ ]" is already defined at level 0
with arguments constr while it is now required to be at level 1
with arguments constr.

This is a problem for me because some libraries that I would like to use (namely Iris/stdpp) are incompatible with Autosubst since they export ListNotations. I would suggest that if Autosubst is going to define notations that clash with standard ones they should be hidden in a module so the user can decide whether to import them or not.