Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

1 files changed, 13 insertions, 0 deletions

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.