8 files changed, 116 insertions, 0 deletions
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
new file mode 100644
index 0000000000..34558e9a6b
--- /dev/null
+++ b/test-suite/output/Binder.out
@@ -0,0 +1,8 @@
+foo = fun '(x, y) => x + y
+     : nat * nat -> nat
+forall '(a, b), a /\ b
+     : Prop
+foo = λ '(x, y), x + y
+     : nat * nat → nat
+∀ '(a, b), a ∧ b
+     : Prop
diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v
new file mode 100644
index 0000000000..9aced9f665
--- /dev/null
+++ b/test-suite/output/Binder.v
@@ -0,0 +1,7 @@
+Definition foo '(x,y) := x + y.
+Print foo.
+Check forall '(a,b), a /\ b.
+
+Require Import Utf8.
+Print foo.
+Check forall '(a,b), a /\ b.
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d38372..d9ce42c606 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,7 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+% i
+     : nat -> nat
+% j
+     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7d..3cf89818d9 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check bug #4854 *)
+Notation "% i" := (fun i : nat => i) (at level 0, i ident).
+Check %i.
+Check %j.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
new file mode 100644
index 0000000000..6a28475d7b
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.out
@@ -0,0 +1,31 @@
+swap = fun '(x, y) => (y, x)
+     : A * B -> B * A
+fun '(x, y) => (y, x)
+     : A * B -> B * A
+forall '(x, y), swap (x, y) = (y, x)
+     : Prop
+proj_informative = fun 'exist _ x _ => x : A
+     : {x : A | P x} -> A
+foo = fun 'Bar n b tt p => if b then n + p else n - p
+     : Foo -> nat
+baz = 
+fun 'Bar n1 _ tt p1 => fun 'Bar _ _ tt _ => n1 + p1
+     : Foo -> Foo -> nat
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
+     : Prop
+swap = 
+fun (A B : Type) (pat : A * B) => let '(x, y) := pat in (y, x)
+     : forall A B : Type, A * B -> B * A
+
+Arguments A, B are implicit and maximally inserted
+Argument scopes are [type_scope type_scope _]
+forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
+     : Prop
+exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+     : Prop
+both_z = 
+fun pat : nat * nat =>
+let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
+     : forall pat : nat * nat, F pat
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
new file mode 100644
index 0000000000..8911909abc
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.v
@@ -0,0 +1,54 @@
+(** The purpose of this file is to test printing of the destructive
+    patterns used in binders ([fun] and [forall]). *)
+
+Parameters (A B : Type) (P:A->Prop).
+
+Definition swap '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun '((x,y) : A*B) => (y,x).
+
+Check forall '(x,y), swap (x,y) = (y,x).
+
+Definition proj_informative '(exist _ x _ : { x:A | P x }) : A := x.
+Print proj_informative.
+
+Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo.
+Definition foo '(Bar n b tt p) :=
+  if b then n+p else n-p.
+Print foo.
+
+Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1.
+Print baz.
+
+(** Some test involving unicode noations. *)
+Module WithUnicode.
+
+  Require Import Coq.Unicode.Utf8.
+
+  Check λ '((x,y) : A*B),  (y,x).
+  Check ∀ '(x,y), swap (x,y) = (y,x).
+
+End WithUnicode.
+
+
+(** * Suboptimal printing *)
+
+(** These tests show examples which expose the [let] introduced by
+    the pattern notation in binders. *)
+
+Module Suboptimal.
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
+
+Check exists '((x,y):A*A), swap (x,y) = (y,x).
+
+Inductive Fin (n:nat) := Z : Fin n.
+Definition F '(n,p) : Type := (Fin n * Fin p)%type.
+Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
+Print both_z.
+
+End Suboptimal.
diff --git a/test-suite/output/onlyprinting.out b/test-suite/output/onlyprinting.out
new file mode 100644
index 0000000000..e0a30fcf6b
--- /dev/null
+++ b/test-suite/output/onlyprinting.out
@@ -0,0 +1,2 @@
+0:-) 0
+     : nat
diff --git a/test-suite/output/onlyprinting.v b/test-suite/output/onlyprinting.v
new file mode 100644
index 0000000000..1973385a0a
--- /dev/null
+++ b/test-suite/output/onlyprinting.v
@@ -0,0 +1,5 @@
+Reserved Notation "x :-) y" (at level 50, only printing).
+
+Notation "x :-) y" := (plus x y).
+
+Check 0 + 0.