2 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index beba8df9..66307236 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -127,3 +127,12 @@ Identifier 'foo' now a keyword
      : nat
 fun _ : nat => 9
      : nat -> nat
+Identifier 'ONE' now a keyword
+fun (x : nat) (p : x = x) => match p with
+                             | ONE => ONE
+                             end = p
+     : forall x : nat, x = x -> Prop
+fun (x : nat) (p : x = x) => match p with
+                             | 1 => 1
+                             end = p
+     : forall x : nat, x = x -> Prop
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 52f499ab..612b5325 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -262,3 +262,16 @@ Notation "'foo' n" := (S n) (at level 50): nat_scope.
 
 Check (foo 9).
 Check (fun _ : nat => 9).
+
+(* Checking parsing and printing of numerical and non-numerical notations for eq_refl *)
+
+(* This notation was not correctly printed until Pierre B.'s
+   improvements to the interpretation of patterns *)
+
+Notation "'ONE'" := eq_refl.
+Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
+
+(* This one used to failed at parsing until now *)
+
+Notation "1" := eq_refl.
+Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.