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

22 files changed, 319 insertions, 154 deletions

diff --git a/CHANGES b/CHANGES
index da9a68926..3f0574762 100644
--- a/CHANGES
+++ b/CHANGES
@@ -114,6 +114,7 @@ Specification language
 - Binders given before ":" in lemmas and in definitions built by tactics are
   now automatically introduced (possible source of incompatibility that can
   be resolved by invoking "Unset Automatic Introduction").
+- New support for multiple implicit arguments signatures per reference.
 
 Module system
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 13aef43c7..206607911 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1205,6 +1205,19 @@ When in a module, tells not to activate the implicit arguments of
 {\qualid} declared by this commands to contexts that requires the
 module.
 
+\item {\tt \zeroone{Global {\sl |} Local} Implicit Arguments {\qualid} \sequence{[ \nelist{\possiblybracketedident}{} ]}{}}
+
+For names of constants, inductive types, constructors, lemmas which
+can only be applied to a fixed number of arguments (this excludes for
+instance constants whose type is polymorphic), multiple lists
+of implicit arguments can be given. These lists must be of different
+length, and, depending on the number of arguments {\qualid} is applied
+to in practice, the longest applicable list of implicit arguments is
+used to select which implicit arguments are inserted.
+
+For printing, the omitted arguments are the ones of the longest list
+of implicit arguments of the sequence.
+
 \end{Variants}
 
 \Example
@@ -1228,6 +1241,8 @@ Fixpoint length (A:Type) (l:list A) : nat :=
 Implicit Arguments map [A B].
 Implicit Arguments length [[A]]. (* A has to be maximally inserted *)
 Check (fun l:list (list nat) => map length l).
+Implicit Arguments map [A B] [A] [].
+Check (fun l => map length l = map (list nat) nat length l).
 \end{coq_example}
 
 \Rem To know which are the implicit arguments of an object, use the command
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6022e1007..eb779200c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -526,7 +526,7 @@ let rec extern inctx scopes vars r =
     extern_symbol scopes vars r'' (uninterp_notations r'')
   with No_match -> match r' with
   | RRef (loc,ref) ->
-      extern_global loc (implicits_of_global ref)
+      extern_global loc (select_stronger_impargs (implicits_of_global ref))
         (extern_reference loc vars ref)
 
   | RVar (loc,id) -> CRef (Ident (loc,id))
@@ -579,7 +579,8 @@ let rec extern inctx scopes vars r =
 		 CRecord (loc, None, List.rev (ip projs locals args []))
 	       with
 		 | Not_found | No_match | Exit ->
-		     extern_app loc inctx (implicits_of_global ref)
+		     extern_app loc inctx
+		       (select_stronger_impargs (implicits_of_global ref))
 		       (Some ref,extern_reference rloc vars ref) args
 	     end
 	 | _       ->
@@ -752,12 +753,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	      let subscopes =
 		try list_skipn n (find_arguments_scope ref) with _ -> [] in
 	      let impls =
-		try list_skipn n (implicits_of_global ref) with _ -> [] in
+		let impls =
+		  select_impargs_size
+		    (List.length args) (implicits_of_global ref) in
+		try list_skipn n impls with _ -> [] in
 	      (if n = 0 then f else RApp (dummy_loc,f,args1)),
 	      args2, subscopes, impls
 	  | RApp (_,(RRef (_,ref) as f),args), None ->
 	      let subscopes = find_arguments_scope ref in
-	      let impls = implicits_of_global ref in
+	      let impls =
+		  select_impargs_size
+		    (List.length args) (implicits_of_global ref) in
 	      f, args, subscopes, impls
 	  | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
           | _, None -> t, [], [], []
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6316228e7..c651d11cb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -39,7 +39,7 @@ type var_internalization_data =
        in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
     identifier list *
     (* signature of impargs of the variable *)
-    Impargs.implicits_list *
+    Impargs.implicit_status list *
     (* subscopes of the args of the variable *)
     scope_name option list
 
@@ -555,7 +555,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
-    RVar (loc,id), impls, argsc, expl_impls
+    RVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
   if Idset.mem id ids or List.mem id ltacvars
@@ -596,7 +596,7 @@ let find_appl_head_data = function
   | RApp (_,RRef (_,ref),l) as x
       when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
-      x,list_skipn_at_least n (implicits_of_global ref),
+      x,List.map (drop_first_implicits n) (implicits_of_global ref),
       list_skipn_at_least n (find_arguments_scope ref),[]
   | x -> x,[],[],[]
 
@@ -1371,6 +1371,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	    it_mkRLambda ibind body
 
   and intern_impargs c env l subscopes args =
+    let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
     let rec aux n impl subscopes eargs rargs =
       let (enva,subscopes') = apply_scope_env env subscopes in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index c0df39aca..6e977056c 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -48,7 +48,7 @@ type var_internalization_data =
     identifier list *
       (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
           in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-    Impargs.implicits_list * (** signature of impargs of the variable *)
+    Impargs.implicit_status list * (** signature of impargs of the variable *)
     scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
diff --git a/lib/util.ml b/lib/util.ml
index 7e62f7703..fb271ea42 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -141,7 +141,7 @@ let string_string_contains ~where ~what =
   with
       Not_found -> false
 
-let plural n s = if n>1 then s^"s" else s
+let plural n s = if n<>1 then s^"s" else s
 
 let ordinal n =
   let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
@@ -1292,29 +1292,28 @@ let pr_vertical_list pr = function
   | [] -> str "none" ++ fnl ()
   | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
 
-let prvecti elem v =
-  let n = Array.length v in
+(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs
+   [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *)
+
+let prvecti_with_sep sep elem v =
   let rec pr i =
     if i = 0 then
       elem 0 v.(0)
     else
-      let r = pr (i-1) and e = elem i v.(i) in r ++ e
+      let r = pr (i-1) and s = sep () and e = elem i v.(i) in
+      r ++ s ++ e
   in
+  let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)
+
+let prvecti elem v = prvecti_with_sep mt elem v
+
 (* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs
    [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
 
-let prvect_with_sep sep elem v =
-  let rec pr n =
-    if n = 0 then
-      elem v.(0)
-    else
-      let r = pr (n-1) and s = sep() and e = elem v.(n) in
-      r ++ s ++ e
-      in
-  let n = Array.length v in
-  if n = 0 then mt () else pr (n - 1)
+let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 
 (* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 83fac5fcd..13be5521d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -348,7 +348,9 @@ val prlist_with_sep :
 val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prvect_with_sep :
-   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
+   (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti_with_sep :
+   (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
diff --git a/library/impargs.ml b/library/impargs.ml
index 19f7e094e..615b568b3 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -27,14 +27,12 @@ open Namegen
 type implicits_flags = {
   auto : bool;                     (* automatic or manual only *)
   strict : bool;                   (* true = strict *)
-  strongly_strict : bool;            (* true = strongly strict *)
+  strongly_strict : bool;          (* true = strongly strict *)
   reversible_pattern : bool;
   contextual : bool;               (* true = contextual *)
   maximal : bool
 }
 
-(* les implicites sont stricts par défaut en v8 *)
-
 let implicit_args = ref {
   auto = false;
   strict = true;
@@ -196,6 +194,17 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   in
   frec true (env,1) m; acc
 
+let rec is_rigid_head t = match kind_of_term t with
+  | Rel _ | Evar _ -> false
+  | Ind _ | Const _ | Var _ | Sort _ -> true
+  | Case (_,_,f,_) -> is_rigid_head f
+  | App (f,args) ->
+      (match kind_of_term f with
+	| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
+	| _ -> is_rigid_head f)
+  | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
+  | Prod _ | Meta _ | Cast _ -> assert false
+
 (* calcule la liste des arguments implicites *)
 
 let find_displayed_name_in all avoid na b =
@@ -205,6 +214,7 @@ let find_displayed_name_in all avoid na b =
     compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
+  let rigid = ref true in
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
@@ -213,6 +223,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ ->
+	  rigid := is_rigid_head t;
 	  let names = List.rev names in
 	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
 	  if contextual then
@@ -223,8 +234,66 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
     | Prod (na,a,b) ->
 	let na',avoid = find_displayed_name_in all [] na b in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
-	Array.to_list v
-    | _ -> []
+	!rigid, Array.to_list v
+    | _ -> true, []
+
+let compute_implicits_flags env f all t =
+  compute_implicits_gen
+    (f.strict or f.strongly_strict) f.strongly_strict
+    f.reversible_pattern f.contextual all env t
+
+let compute_auto_implicits env flags enriching t =
+  if enriching then compute_implicits_flags env flags true t
+  else compute_implicits_gen false false false true true env t
+
+(* Extra information about implicit arguments *)
+
+type maximal_insertion = bool (* true = maximal contextual insertion *)
+type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
+
+type implicit_status =
+    (* None = Not implicit *)
+    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
+
+type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
+
+type implicits_list = implicit_side_condition * implicit_status list
+
+let is_status_implicit = function
+  | None -> false
+  | _ -> true
+
+let name_of_implicit = function
+  | None -> anomaly "Not an implicit argument"
+  | Some (id,_,_) -> id
+
+let maximal_insertion_of = function
+  | Some (_,_,(b,_)) -> b
+  | None -> anomaly "Not an implicit argument"
+
+let force_inference_of = function
+  | Some (_, _, (_, b)) -> b
+  | None -> anomaly "Not an implicit argument"
+
+(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
+let is_inferable_implicit in_ctx n = function
+  | None -> false
+  | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
+  | Some (_,DepFlex (Hyp p),_) -> false
+  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q
+  | Some (_,DepRigid Conclusion,_) -> in_ctx
+  | Some (_,DepFlex Conclusion,_) -> false
+  | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
+  | Some (_,Manual,_) -> true
+
+let positions_of_implicits (_,impls) =
+  let rec aux n = function
+      [] -> []
+    | Some _ :: l -> n :: aux (n+1) l
+    | None :: l -> aux (n+1) l
+  in aux 1 impls
+
+(* Manage user-given implicit arguments *)
 
 let rec prepare_implicits f = function
   | [] -> []
@@ -234,11 +303,6 @@ let rec prepare_implicits f = function
       Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
-let compute_implicits_flags env f all t =
-  compute_implicits_gen
-    (f.strict or f.strongly_strict) f.strongly_strict
-    f.reversible_pattern f.contextual all env t
-
 let set_implicit id imp insmax =
   (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
@@ -247,11 +311,20 @@ let rec assoc_by_pos k = function
   | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
   | [] -> raise Not_found
 
-let compute_manual_implicits env flags t enriching l =
-  let autoimps =
-    if enriching then compute_implicits_flags env flags true t
-    else compute_implicits_gen false false false true true env t in
-  let n = List.length autoimps in
+let check_correct_manual_implicits autoimps l =
+  List.iter (function
+    | ExplByName id,(b,fi,forced) ->
+	if not forced then
+	  error ("Wrong or non-dependent implicit argument name: "^(string_of_id id)^".")
+    | ExplByPos (i,_id),_t ->
+	if i<1 or i>List.length autoimps then
+	  error ("Bad implicit argument number: "^(string_of_int i)^".")
+	else
+	  errorlabstrm ""
+	    (str "Cannot set implicit argument number " ++ int i ++
+	      str ": it has no name.")) l
+
+let set_manual_implicits env flags enriching autoimps l =
   let try_forced k l =
     try
       let (id, (b, fi, fo)), l' = assoc_by_pos k l in
@@ -262,7 +335,7 @@ let compute_manual_implicits env flags t enriching l =
     with Not_found -> l, None
   in
   if not (list_distinct l) then
-    error ("Some parameters are referred more than once");
+    error ("Some parameters are referred more than once.");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
   | (Name id,imp)::imps ->
@@ -285,79 +358,28 @@ let compute_manual_implicits env flags t enriching l =
 	forced :: merge (k+1) l' imps
   | [] when l = [] -> []
   | [] ->
-      List.iter (function
-	| ExplByName id,(b,fi,forced) ->
-	    if not forced then
-	      error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
-	| ExplByPos (i,_id),_t ->
-	    if i<1 or i>n then
-	      error ("Bad implicit argument number: "^(string_of_int i))
-	    else
-	      errorlabstrm ""
-		(str "Cannot set implicit argument number " ++ int i ++
-		    str ": it has no name"))
-	l; []
+      check_correct_manual_implicits autoimps l;
+      []
   in
   merge 1 l autoimps
 
-let compute_implicits_auto env f manual t =
+let compute_semi_auto_implicits env f manual t =
   match manual with
   | [] ->
       if not f.auto then []
-      else let l = compute_implicits_flags env f false t in
-	     prepare_implicits f l
-  | _ -> compute_manual_implicits env f t f.auto manual
-
-let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
-
-type maximal_insertion = bool (* true = maximal contextual insertion *)
-type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
-
-type implicit_status =
-    (* None = Not implicit *)
-    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
-
-type implicits_list = implicit_status list
-
-let is_status_implicit = function
-  | None -> false
-  | _ -> true
-
-let name_of_implicit = function
-  | None -> anomaly "Not an implicit argument"
-  | Some (id,_,_) -> id
-
-let maximal_insertion_of = function
-  | Some (_,_,(b,_)) -> b
-  | None -> anomaly "Not an implicit argument"
-
-let force_inference_of = function
-  | Some (_, _, (_, b)) -> b
-  | None -> anomaly "Not an implicit argument"
-
-(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
-let is_inferable_implicit in_ctx n = function
-  | None -> false
-  | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
-  | Some (_,DepFlex (Hyp p),_) -> false
-  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q
-  | Some (_,DepRigid Conclusion,_) -> in_ctx
-  | Some (_,DepFlex Conclusion,_) -> false
-  | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
-  | Some (_,Manual,_) -> true
+      else let _,l = compute_implicits_flags env f false t in
+	     [DefaultImpArgs, prepare_implicits f l]
+  | _ ->
+      let _,autoimpls = compute_auto_implicits env f f.auto t in
+      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
 
-let positions_of_implicits =
-  let rec aux n = function
-      [] -> []
-    | Some _ :: l -> n :: aux (n+1) l
-    | None :: l -> aux (n+1) l
-  in aux 1
+let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t
 
 (*s Constants. *)
 
 let compute_constant_implicits flags manual cst =
   let env = Global.env () in
-  compute_implicits_auto env flags manual (Typeops.type_of_constant env cst)
+  compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst)
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -377,9 +399,9 @@ let compute_mib_implicits flags manual kn =
   let imps_one_inductive i mip =
     let ind = (kn,i) in
     let ar = type_of_inductive env (mib,mip) in
-    ((IndRef ind,compute_implicits_auto env flags manual ar),
+    ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
      Array.mapi (fun j c ->
-       (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c))
+       (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
        mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
@@ -394,7 +416,7 @@ let compute_all_mib_implicits flags manual kn =
 let compute_var_implicits flags manual id =
   let env = Global.env () in
   let (_,_,ty) = lookup_named id env in
-  compute_implicits_auto env flags manual ty
+  compute_semi_auto_implicits env flags manual ty
 
 (* Implicits of a global reference. *)
 
@@ -408,12 +430,15 @@ let compute_global_implicits flags manual = function
 
 (* Merge a manual explicitation with an implicit_status list *)
 
-let merge_impls oldimpls newimpls =
-  List.map2 (fun orig ni ->
+let merge_one_impls_block (cond,oldimpls) (_,newimpls) =
+  cond, List.map2 (fun orig ni ->
     match orig with
     | Some (_, Manual, _) -> orig
     | _ -> ni) oldimpls newimpls
 
+let merge_impls oldimpls newimpls =
+  List.map2 merge_one_impls_block oldimpls newimpls
+
 (* Caching implicits *)
 
 type implicit_interactive_request =
@@ -456,23 +481,35 @@ let section_segment_of_reference = function
       section_segment_of_mutual_inductive kn
   | _ -> []
 
+let adjust_side_condition p = function
+  | LessArgsThan n -> LessArgsThan (n+p)
+  | DefaultImpArgs -> DefaultImpArgs
+
+let add_section_impls vars extra_impls (cond,impls)=
+  let p = List.length vars - List.length extra_impls in
+  adjust_side_condition p cond, extra_impls @ impls
+
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
       let vars = section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
-      let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
+      let extra_impls = impls_of_context vars in
+      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
   | ImplConstant (con,flags) ->
       let con' = pop_con con in
-      let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in
+      let vars = section_segment_of_constant con in
+      let extra_impls = impls_of_context vars in
+      let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
 	Some (ImplConstant (con',flags),l')
   | ImplMutualInductive (kn,flags) ->
       let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
+	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
-	 impls_of_context vars @ l)) l
+	 List.map (add_section_impls vars extra_impls) l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
@@ -504,7 +541,9 @@ let rebuild_implicits (req,l) =
 	  let oldimpls = snd (List.hd l) in
 	  if flags.auto then
 	    let newimpls = compute_global_implicits flags [] ref in
-	    [ref, merge_impls oldimpls newimpls]
+	    assert (List.tl newimpls = []);
+	    let newimpls = List.map (fun _ -> List.hd newimpls) oldimpls in
+	    [ref,merge_impls oldimpls newimpls]
 	  else
 	    [ref,oldimpls]
 
@@ -552,14 +591,42 @@ let declare_mib_implicits kn =
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
 let compute_implicits_with_manual env typ enriching l =
-  compute_manual_implicits env !implicit_args typ enriching l
+  let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in
+  set_manual_implicits env !implicit_args enriching autoimpls l
+
+let check_inclusion l =
+  (* Check strict inclusion *)
+  let rec aux = function
+    | n1::(n2::_ as nl) ->
+	if n1 <= n2 then
+	  error "Sequences of implicit arguments must be of different lengths";
+	aux nl
+    | _ -> () in
+  aux (List.map (fun (imps,_) -> List.length imps) l)
+
+let check_rigidity isrigid =
+  if not isrigid then
+    errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
   let enriching = Option.default flags.auto enriching in
-  let l' = compute_manual_implicits env flags t enriching l in
+  let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
+  let l' = match l with
+    | [] -> assert false
+    | [l] ->
+	[DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l]
+    | _ ->
+	check_rigidity isrigid;
+	let l = List.map (fun imps -> (imps,List.length imps)) l in
+	let l = Sort.list (fun (_,n1) (_,n2) -> n1 > n2) l in
+	check_inclusion l;
+	let nargs = List.length autoimpls in
+	List.map (fun (imps,n) ->
+	  (LessArgsThan (nargs-n),
+	   set_manual_implicits env flags enriching autoimpls imps)) l in
   let req =
     if is_local local ref then ImplLocal
     else ImplInteractive(ref,flags,ImplManual)
@@ -568,7 +635,14 @@ let declare_manual_implicits local ref ?enriching l =
 
 let maybe_declare_manual_implicits local ref ?enriching l =
   if l = [] then ()
-  else declare_manual_implicits local ref ?enriching l
+  else declare_manual_implicits local ref ?enriching [l]
+
+let extract_impargs_data impls =
+  let rec aux p = function
+    | (DefaultImpArgs, imps)::_ -> [None,imps]
+    | (LessArgsThan n, imps)::l -> (Some (p,n),imps) :: aux (n+1) l
+    | [] -> [] in
+  aux 0 impls
 
 let lift_implicits n =
   List.map (fun x ->
@@ -576,6 +650,24 @@ let lift_implicits n =
 	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
       | _ -> x)
 
+let make_implicits_list l = [DefaultImpArgs, l]
+
+let rec drop_first_implicits p = function
+  | _,[] as x -> x
+  | DefaultImpArgs,imp::impls ->
+      drop_first_implicits (p-1) (DefaultImpArgs,impls)
+  | LessArgsThan n,imp::impls ->
+      let n = if is_status_implicit imp then n-1 else n in
+      drop_first_implicits (p-1) (LessArgsThan n,impls)
+
+let rec select_impargs_size n = function
+  | [] -> []
+  | [_, impls] | (DefaultImpArgs, impls)::_ -> impls
+  | (LessArgsThan p, impls)::l ->
+      if n <= p then impls else select_impargs_size n l
+
+let rec select_stronger_impargs = function [] -> [] | (_,impls)::_ -> impls
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index 84f327563..f71607ec9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -51,7 +51,7 @@ type implicit_explanation =
   | Manual
 
 type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
-type implicits_list = implicit_status list
+type implicits_list (* = implicit_status list *)
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
@@ -61,17 +61,13 @@ val force_inference_of : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
-(** Computation of the positions of arguments automatically inferable
-   for an object of the given type in the given env *)
-val compute_implicits : env -> types -> implicits_list
-
 (** A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion, force inference and force usage flags. Forcing usage makes
    the argument implicit even if the automatic inference considers it not inferable. *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool ->
-  manual_explicitation list -> implicits_list
+  manual_explicitation list -> implicit_status list
 
 (** {6 Computation of implicits (done using the global environment). } *)
 
@@ -88,22 +84,29 @@ val declare_implicits : bool -> global_reference -> unit
    Unsets implicits if [l] is empty. *)
 
 val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_explicitation list -> unit
+  manual_explicitation list list -> unit
 
 (** If the list is empty, do nothing, otherwise declare the implicits. *)
 
 val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
   manual_explicitation list -> unit
 
-val implicits_of_global : global_reference -> implicits_list
+val implicits_of_global : global_reference -> implicits_list list
+
+val extract_impargs_data :
+  implicits_list list -> ((int * int) option * implicit_status list) list
 
 val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
 
-val merge_impls : implicits_list -> implicits_list -> implicits_list
+val make_implicits_list : implicit_status list -> implicits_list list
+
+val drop_first_implicits : int -> implicits_list -> implicits_list
+
+val select_impargs_size : int -> implicits_list list -> implicit_status list
+
+val select_stronger_impargs : implicits_list list -> implicit_status list
 
-type implicit_interactive_request =
-  | ImplAuto
-  | ImplManual
+type implicit_interactive_request
 
 type implicit_discharge_request =
   | ImplLocal
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 329269e87..08862f044 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -556,7 +556,7 @@ GEXTEND Gram
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
-	   pos = OPT [ "["; l = LIST0 implicit_name; "]" ->
+	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ba3371ee3..269f81699 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -801,13 +801,15 @@ let rec pr_vernac = function
         (pr_locality local ++ str"Notation " ++ pr_lident id ++
 	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
-  | VernacDeclareImplicits (local,q,None) ->
+  | VernacDeclareImplicits (local,q,[]) ->
       hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ 
 	pr_smart_global q)
-  | VernacDeclareImplicits (local,q,Some imps) ->
+  | VernacDeclareImplicits (local,q,impls) ->
       hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ 
 	spc() ++ pr_smart_global q ++ spc() ++
-	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+	prlist_with_sep spc (fun imps ->
+	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+	  impls)
   | VernacReserve bl ->
       let n = List.length (List.flatten (List.map fst bl)) in
       hov 2 (str"Implicit Type" ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index d1a42a021..4ea3b1591 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -59,6 +59,10 @@ let with_line_skip l = if l = [] then mt() else fnl() ++ pr_infos_list l
 
 let blankline = mt() (* add a blank sentence in the list of infos *)
 
+let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": "
+
+let int_or_no n = if n=0 then str "no" else int n
+
 (*******************)
 (** Basic printing *)
 
@@ -88,13 +92,33 @@ let print_impargs_by_name max = function
       str (conjugate_verb_to_be impls) ++ str" implicit" ++
       (if max then strbrk " and maximally inserted" else mt()))]
 
-let print_impargs_list l =
+let print_one_impargs_list l =
   let imps = List.filter is_status_implicit l in
   let maximps = List.filter Impargs.maximal_insertion_of imps in
   let nonmaximps = list_subtract imps maximps in
   print_impargs_by_name false nonmaximps @
   print_impargs_by_name true maximps
 
+let print_impargs_list prefix l =
+  let l = extract_impargs_data l in
+  List.flatten (List.map (fun (cond,imps) ->
+    match cond with
+    | None ->
+	List.map (fun pp -> add_colon prefix ++ pp)
+	  (print_one_impargs_list imps)
+    | Some (n1,n2) ->
+       [v 2 (prlist_with_sep cut (fun x -> x)
+	 [(if ismt prefix then str "When" else prefix ++ str ", when") ++
+	   str " applied to " ++
+	   (if n1 = n2 then int_or_no n2 else
+	    if n1 = 0 then str "less than " ++ int n2
+	    else int n1 ++ str " to " ++ int_or_no n2) ++
+	    str (plural n2 " argument") ++ str ":";
+          v 0 (prlist_with_sep cut (fun x -> x)
+	    (if List.exists is_status_implicit imps
+	    then print_one_impargs_list imps
+	    else [str "No implicit arguments"]))])]) l)
+
 let need_expansion impl ref =
   let typ = Global.type_of_global ref in
   let ctx = (prod_assum typ) in
@@ -106,20 +130,22 @@ let need_expansion impl ref =
 let print_impargs ref =
   let ref = Smartlocate.smart_global ref in
   let impl = implicits_of_global ref in
-  let has_impl = List.filter is_status_implicit impl <> [] in
+  let has_impl = impl <> [] in
   (* Need to reduce since implicits are computed with products flattened *)
   pr_infos_list
-    ([ print_ref (need_expansion impl ref) ref; blankline ] @
-    (if has_impl then print_impargs_list impl
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+       blankline ] @
+    (if has_impl then print_impargs_list (mt()) impl
      else [str "No implicit arguments"]))
 
 (*********************)
 (** Printing Scopes  *)
 
-let print_argument_scopes = function
-  | [Some sc] -> [str"Argument scope is [" ++ str sc ++ str"]"]
+let print_argument_scopes prefix = function
+  | [Some sc] ->
+      [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"]
   | l when not (List.for_all ((=) None) l) ->
-     [hov 2 (str"Argument scopes are" ++ spc() ++
+     [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
       str "[" ++
       prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++
       str "]")]
@@ -163,23 +189,22 @@ let print_opacity ref =
 (* *)
 
 let print_name_infos ref =
-  let impl = implicits_of_global ref in
+  let impls = implicits_of_global ref in
   let scopes = Notation.find_arguments_scope ref in
   let type_info_for_implicit =
-    if need_expansion impl ref then
+    if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
       [str "Expanded type for implicit arguments";
        print_ref true ref; blankline]
     else
       [] in
   type_info_for_implicit @
-  print_impargs_list impl @
-  print_argument_scopes scopes
+  print_impargs_list (mt()) impls @
+  print_argument_scopes (mt()) scopes
 
 let print_id_args_data test pr id l =
   if List.exists test l then
-    List.map (fun pp -> str"For " ++ pr_id id ++ str": " ++ pp)
-      (List.filter (fun x -> not (ismt x)) (pr l))
+    pr (str "For " ++ pr_id id) l
   else
     []
 
@@ -195,7 +220,8 @@ let print_args_data_of_inductive_ids get test pr sp mipv =
 
 let print_inductive_implicit_args =
   print_args_data_of_inductive_ids
-    implicits_of_global is_status_implicit print_impargs_list
+    implicits_of_global (fun l -> positions_of_implicits l <> [])
+    print_impargs_list
 
 let print_inductive_argument_scopes =
   print_args_data_of_inductive_ids
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 8a47dab7c..4a244553e 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -79,7 +79,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
     Lemmas.start_proof id kind c (fun loc gr ->
-      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
+      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
       hook loc gr)
 
 let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 1db9d407d..a663d3db3 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -171,7 +171,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let hook vis gr =
     let cst = match gr with ConstRef kn -> kn | _ -> assert false in
     let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
-      Impargs.declare_manual_implicits false gr ~enriching:false imps;
+      Impargs.declare_manual_implicits false gr ~enriching:false [imps];
       Typeclasses.add_instance inst
   in
   let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 397bda9b0..eb3abfa5a 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -332,7 +332,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || impls <> [] then
-	    Impargs.declare_manual_implicits false gr impls
+	    Impargs.declare_manual_implicits false gr [impls]
       in
       let typ = it_mkProd_or_LetIn top_arity binders in
 	hook, name, typ
@@ -340,7 +340,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
       let hook l gr = 
 	if Impargs.is_implicit_args () || impls <> [] then
-	  Impargs.declare_manual_implicits false gr impls
+	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
   let fullcoqc = Evarutil.nf_evar !isevars def in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 22cc745f6..d61ca2bc8 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -211,7 +211,7 @@ let declare_definition prg =
 	in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
-	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
+	    Impargs.declare_manual_implicits false gr [prg.prg_implicits];
 	  print_message (Subtac_utils.definition_message prg.prg_name);
 	  progmap_remove prg; 
 	  prg.prg_hook local gr;
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.
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0822e6977..d67c022a1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -318,8 +318,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	  (DefinitionEntry proj_entry, IsDefinition Definition)
 	in
 	let cref = ConstRef cst in
-	Impargs.declare_manual_implicits false cref paramimpls;
-	Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
+	Impargs.declare_manual_implicits false cref [paramimpls];
+	Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
 	Classes.set_typeclass_transparency (EvalConstRef cst) false;
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
 	cref, [Name proj_name, Some proj_cst]
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0404e18c..c6071eb96 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -760,11 +760,11 @@ let vernac_syntactic_definition lid =
   Metasyntax.add_syntactic_definition (snd lid)
 
 let vernac_declare_implicits local r = function
-  | Some imps ->
-      Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
-	(List.map (fun (ex,b,f) -> ex, (b,true,f)) imps)
-  | None ->
+  | [] ->
       Impargs.declare_implicits local (smart_global r)
+  | _::_ as imps ->
+      Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
+	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 224d9765f..50fb61eba 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -310,7 +310,7 @@ type vernac_expr =
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
-      (explicitation * bool * bool) list option
+      (explicitation * bool * bool) list list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of locality_flag * (lident list) option
   | VernacSetOpacity of