Used multiple lists of implicit arguments to transfer the choices of

Program in terms of implicit arguments to the rest of the library.
This commit only covers the case of list of implicit arguments that
have a different length in Program (e.g. inl, Vcons) but not the case of
implicit arguments which differs only in their maximality status
(e.g. pair).

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

7 files changed, 15 insertions, 17 deletions

diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 88bc15c69..694ed15b4 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -249,3 +249,6 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   end.
 
 End BOOLEAN_VECTORS.
+
+Implicit Arguments Vcons [[A] [n]] [].
+Implicit Arguments Vnil [[A]] [].
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 3ad4ce847..184839eff 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -153,6 +153,9 @@ Inductive sum (A B:Type) : Type :=
 
 Notation "x + y" := (sum x y) : type_scope.
 
+Implicit Arguments inl [[A] [B]] [A].
+Implicit Arguments inr [[A] [B]] [B].
+
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
 
@@ -164,6 +167,8 @@ Add Printing Let prod.
 Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
+Implicit Arguments pair [[A] [B]].
+
 Section projections.
   Variables A B : Type.
   Definition fst (p:A * B) := match p with
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 24385e7fc..c72193c0b 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -267,7 +267,8 @@ Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (x <> y :>_) : type_scope.
 
-Implicit Arguments eq [ [A] ].
+Implicit Arguments eq [[A]].
+Implicit Arguments eq_refl [[A] [x]] [A].
 
 Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index df98d369b..a871c4081 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -126,6 +126,9 @@ Inductive sumbool (A B:Prop) : Set :=
 
 Add Printing If sumbool.
 
+Implicit Arguments left [[A] [B]] [A].
+Implicit Arguments right [[A] [B]] [B].
+
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
 
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 4e9f46b7c..583d348a2 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -24,6 +24,8 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
 
 Set Elimination Schemes.
 
+Implicit Arguments JMeq_refl [[A] [x]] [A].
+
 Hint Resolve JMeq_refl.
 
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 2f0185eac..d678757d9 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -37,11 +37,6 @@ Ltac unblock_goal := unfold block in *.
 
 Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
-(** Notation for the single element of [x = x] and [x ~= x]. *)
-
-Implicit Arguments eq_refl [[A] [x]] [A].
-Implicit Arguments JMeq_refl [[A] [x]] [A].
-
 (** Do something on an heterogeneous equality appearing in the context. *)
 
 Ltac on_JMeq tac :=
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index fb8dc087b..d66785874 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -21,12 +21,6 @@ Notation " () " := tt.
 Implicit Arguments Some [[A]].
 Implicit Arguments None [[A]].
 
-Implicit Arguments inl [[A] [B]] [A].
-Implicit Arguments inr [[A] [B]] [B].
-
-Implicit Arguments left [[A] [B]] [A].
-Implicit Arguments right [[A] [B]] [B].
-
 Implicit Arguments pair [[A] [B]].
 Implicit Arguments fst [[A] [B]].
 Implicit Arguments snd [[A] [B]].
@@ -40,13 +34,8 @@ Notation " [ ] " := nil : list_scope.
 Notation " [ x ] " := (cons x nil) : list_scope.
 Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
-(** Implicit arguments for vectors. *)
-
 Require Import Bvector.
 
-Implicit Arguments Vnil [[A]] [].
-Implicit Arguments Vcons [[A] [n]] [].
-
 (** Treating n-ary exists *)
 
 Tactic Notation "exists" constr(x) := exists x.