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

1 files changed, 5 insertions, 0 deletions

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