Adapting the output test Notations:

- unbound variables in notation are allowed, forcing only parsing mode
- plus and mult are now themselves abbreviations
- evars are named

2 files changed, 7 insertions, 8 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 54b4939e6..d81a71e4a 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -54,8 +54,6 @@ term position as part of a recursive pattern.
 The command has indeed failed with message:
 => Error: The reference w was not found in the current environment.
 The command has indeed failed with message:
-=> Error: x is unbound in the right-hand side.
-The command has indeed failed with message:
 => Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
@@ -89,11 +87,11 @@ Identifier 'I' now a keyword
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
      : (Z -> Z -> Z -> Z) -> Z
-plus
+Init.Nat.add
      : nat -> nat -> nat
 S
      : nat -> nat
-mult
+Init.Nat.mul
      : nat -> nat -> nat
 le
      : nat -> nat -> Prop
@@ -101,7 +99,7 @@ plus
      : nat -> nat -> nat
 succ
      : nat -> nat
-mult
+Init.Nat.mul
      : nat -> nat -> nat
 le
      : nat -> nat -> Prop
@@ -120,11 +118,11 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?95 => match x with
+fun x : list ?T0 => match x with
                     | NIL => NONE2
                     | (_ :') t => SOME2 t
                     end
-     : list ?95 -> option (list ?95)
+     : list ?T0 -> option (list ?T0)
 s
      : s
 Identifier 'foo' now a keyword
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index bbd35b83b..adba688e6 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -133,7 +133,8 @@ Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
 Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
 
 (* Right-unbound variable *)
-Fail Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+(* Now allowed with an only parsing restriction *)
+Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
 
 (* Not the right kind of recursive pattern *)
 Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).