summaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Notations.out9
-rw-r--r--test-suite/output/Notations.v13
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.