4 files changed, 78 insertions, 0 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 28afd06fbc..ef7667936c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -12,3 +12,8 @@ map id' (1 :: nil)
      : list nat
 map (id'' (A:=nat)) (1 :: nil)
      : list nat
+fix f (x : nat) : option nat := match x with
+                                | 0 => None
+                                | S _ => x
+                                end
+     : nat -> option nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 306532c0df..a7c4399e38 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x.
 
 Check map (@id'' nat) (1::nil).
 
+Module MatchBranchesInContext.
+
+Set Implicit Arguments.
+Set Contextual Implicit.
+
+Inductive option A := None | Some (a:A).
+Coercion some_nat := @Some nat.
+Check fix f x := match x with 0 => None | n => some_nat n end.
+
+End MatchBranchesInContext.
diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
new file mode 100644
index 0000000000..824c260e92
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.out
@@ -0,0 +1,26 @@
+forall b, b = b
+     : Prop
+forall b : nat, b = b
+     : Prop
+forall b : bool, @eq bool b b
+     : Prop
+forall b : bool, b = b
+     : Prop
+forall b c : bool, b = c
+     : Prop
+forall c b : bool, b = c
+     : Prop
+forall b1 b2, b1 = b2
+     : Prop
+fun b => b = b
+     : bool -> Prop
+fix f b (n : nat) {struct n} : bool :=
+  match n with
+  | 0 => b
+  | S p => f b p
+  end
+     : bool -> nat -> bool
+∀ b c : bool, b = c
+     : Prop
+∀ b1 b2, b1 = b2
+     : Prop
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
new file mode 100644
index 0000000000..dbc83f9229
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.v
@@ -0,0 +1,37 @@
+Implicit Types b : bool.
+Check forall b, b = b.
+
+(* Check the type is not used if not the reserved one *)
+Check forall b:nat, b = b.
+
+(* Check full printing *)
+Set Printing All.
+Check forall b, b = b.
+Unset Printing All.
+
+(* Check printing of type *)
+Unset Printing Use Implicit Types.
+Check forall b, b = b.
+Set Printing Use Implicit Types.
+
+(* Check factorization: we give priority on factorization over implicit type *)
+Check forall b c, b = c.
+Check forall c b, b = c.
+
+(* Check factorization of implicit types *)
+Check forall b1 b2, b1 = b2.
+
+(* Check in "fun" *)
+Check fun b => b = b.
+
+(* Check in binders *)
+Check fix f b n := match n with 0 => b | S p => f b p end.
+
+(* Check in notations *)
+Module Notation.
+  Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+    (at level 200, x binder, y binder, right associativity,
+    format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+  Check forall b c, b = c.
+  Check forall b1 b2, b1 = b2.
+End Notation.