1 files changed, 53 insertions, 6 deletions

diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index b37c3638..f041b9b7 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -64,26 +64,26 @@ Open Scope nat_scope.
 
 Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
 Coercion Zpos: nat >-> znat.
- 
+
 Delimit Scope znat_scope with znat.
 Open Scope znat_scope.
- 
+
 Variable addz : znat -> znat -> znat.
 Notation "z1 + z2" := (addz z1 z2) : znat_scope.
 
   (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit,
-     is printed the same way, and not "S 2 + S 2" as if numeral printing was 
+     is printed the same way, and not "S 2 + S 2" as if numeral printing was
      only tested with coercion still present *)
 
 Check (3+3).
 
 (**********************************************************************)
 (* Check recursive notations                                          *)
- 
+
 Require Import List.
 Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
 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).
@@ -102,7 +102,7 @@ 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).
 
-Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := 
+Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" :=
   (match x with O => u | S n => t end) (at level 0, u at level 0).
 Check fun x => ifn x is succ n then n else 0.
 
@@ -121,6 +121,18 @@ Notation "- 4" := (-2 + -2).
 Check -4.
 
 (**********************************************************************)
+(* Check preservation of scopes at printing time *)
+
+Notation SUM := sum.
+Check SUM (nat*nat) nat.
+
+(**********************************************************************)
+(* Check preservation of implicit arguments at printing time *)
+
+Notation FST := fst.
+Check FST (0;1).
+
+(**********************************************************************)
 (* Check notations for references with activated or deactivated       *)
 (* implicit arguments                                                 *)
 
@@ -159,3 +171,38 @@ Check [|1,2,3;4,5,6|].
 
 Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
 Check fun f => {| f; 0; 1; 2 |} : Z.
+
+(**********************************************************************)
+(* Check printing of notations from other modules *)
+
+(* 1- Non imported case *)
+
+Require make_notation.
+
+Check plus.
+Check S.
+Check mult.
+Check le.
+
+(* 2- Imported case *)
+
+Import make_notation.
+
+Check plus.
+Check S.
+Check mult.
+Check le.
+
+(* Check notations in cases patterns *)
+
+Notation SOME := Some.
+Notation NONE := None.
+Check (fun x => match x with SOME x => x | NONE => 0 end).
+
+Notation NONE2 := (@None _).
+Notation SOME2 := (@Some _).     
+Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
+
+Notation NONE3 := @None.
+Notation SOME3 := @Some.     
+Check (fun x => match x with SOME3 x => x | NONE3 => 0 end).