1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 6e637aca..b37c3638 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -129,3 +129,33 @@ Check Nil.
 
 Notation NIL := nil.
 Check NIL : list nat.
+
+
+(**********************************************************************)
+(* Test printing of notation with coercions in scope of a coercion    *)
+
+Open Scope nat_scope.
+
+Coercion is_true := fun b => b=true.
+Coercion of_nat n := match n with 0 => true | _ => false end.
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+
+Check (false && I 3)%bool /\ I 6.
+
+(**********************************************************************)
+(* Check notations with several recursive patterns                    *)
+
+Open Scope Z_scope.
+
+Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
+  (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
+Check [|1,2,3;4,5,6|].
+
+(**********************************************************************)
+(* Test recursive notations involving applications                    *)
+(* Caveat: does not work for applied constant because constants are   *)
+(* classified as notations for the particular constant while this     *)
+(* generic application notation is classified as generic              *)
+
+Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+Check fun f => {| f; 0; 1; 2 |} : Z.