5 files changed, 58 insertions, 6 deletions
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 13b5e13d..1ff53294 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -1,4 +1,4 @@
-(* A few tests to check Argument Scope Global command *)
+(* A few tests to check Global Argument Scope command *)
 
 Section A.
 Variable a : bool -> bool.
@@ -11,11 +11,11 @@ About b.
 About negb''.
 About negb'.
 About negb.
-Arguments Scope Global negb'' [ _ ].
-Arguments Scope Global negb' [ _ ].
-Arguments Scope Global negb [ _ ].
-Arguments Scope Global a [ _ ].
-Arguments Scope Global b [ _ ].
+Global Arguments Scope negb'' [ _ ].
+Global Arguments Scope negb' [ _ ].
+Global Arguments Scope negb [ _ ].
+Global Arguments Scope a [ _ ].
+Global Arguments Scope b [ _ ].
 About a.
 About b.
 About negb.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 995754a6..1f0e12d3 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -28,3 +28,5 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
      : forall A : Type, list A -> option A
 
 Argument scopes are [type_scope list_scope]
+foo' = if A 0 then true else false
+     : bool
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 61f89d40..37ee71e9 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -33,3 +33,16 @@ Fixpoint foo (A:Type) (l:list A) : option A :=
   end.
 
 Print foo.
+
+(* Do not duplicate the matched term *)
+
+Axiom A : nat -> bool.
+
+Definition foo' :=
+  match A 0 with
+    | true => true
+    | x => x
+  end.
+
+Print foo'.
+
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2066a7ef..42858304 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,3 +50,10 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
+Defining 'I' as keyword
+(false && I 3)%bool /\ I 6
+     : Prop
+[|1, 2, 3; 4, 5, 6|]
+     : Z * Z * Z * (Z * Z * Z)
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+     : (Z -> Z -> Z -> Z) -> Z
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.