1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 4382975e86..5330e145e6 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -17,12 +17,16 @@ Check (decomp (true,true) as t, u in (t,u)).
 (**********************************************************************)
 (* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
 
+Section A.
+
 Notation "! A" := (forall _:nat, A) (at level 60).
 
 Check ! (0=0).
 Check forall n, n=0.
 Check forall n:nat, 0=0.
 
+End A.
+
 (**********************************************************************)
 (* Conflict between notation and notation below coercions             *)
 
@@ -66,3 +70,13 @@ Check [1;2;4].
 Reserved Notation "( x ; y , .. , z )" (at level 0).
 Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
 Check (1;2,4).
+
+Notation "'ifzero' n" := (match n with 0 => true | S _ => false end)
+  (at level 0, n at level 0).
+Check (ifzero 3).
+
+Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end)
+  (at level 0, n at level 0).
+Check (pred 3).
+Check (fun n => match n with 0 => 0 | S n => n end).
+Check (fun n => match n with S p as x => p | y => 0 end).