From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 test-suite/success/implicit.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'test-suite/success/implicit.v')

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.
-- 
cgit v1.2.3