Printing precedence bug leading to wrong parentheses in custom entries

[herbelin]

Inductive Expr := 
 | Mul : Expr -> Expr -> Expr 
 | Add : Expr -> Expr -> Expr  
 | One : Expr.   
         
Declare Custom Entry expr.    
Notation "[ expr ]" := expr (expr custom expr at level 2). 
Notation "1" := One (in custom expr at level 0).       
Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity).    
Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).  
 
Check Add [1 + 1] [1 + 1].

was wrongly written [1+1+(1+1)] even though parentheses were not declared in the custom expr.

[herbelin]

The printing bug was reported in coq#12775 and coq#13018. It was first fixed in coq#13073 from 8.12, with a more principle fix in coq#17117 for 8.18.

The only interesting commit is the cleanup renaming of "level" into "notation_signature" (c817660).