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

3 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 2c2035004..19d7e7c68 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -78,3 +78,12 @@ Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation existS2 := existT2
 Expands to: Notation Coq.Init.Specif.existS2
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument A is implicit and maximally inserted
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 972caf8aa..dd9f3c07a 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -26,3 +26,6 @@ Print bar.
 
 About Peano. (* Module *)
 About existS2. (* Notation *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+Print eq_refl.
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.