Added multiple implicit arguments rules per name.

Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".

This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 59e1a9352..0aa0ae02b 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -86,3 +86,9 @@ 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.