1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 59e1a935..ce3e692f 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -86,3 +86,24 @@ Fixpoint plus n m {struct n} :=
   | 0 => m
   | S p => S (plus p m)
   end.
+
+(* Check multiple implicit arguments signatures *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+
+Check eq_refl : 0 = 0.
+
+(* Check that notations preserve implicit (since 8.3) *)
+
+Parameter p : forall A, A -> forall n, n = 0 -> True.
+Implicit Arguments p [A n].
+Notation Q := (p 0).
+Check Q eq_refl.
+
+(* Check implicits with Context *)
+
+Section C.
+Context {A:Set}.
+Definition h (a:A) := a.
+End C.
+Check h 0.