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, 15 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6022e10070..eb779200c3 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 6316228e71..c651d11cba 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 c0df39aca8..6e977056cc 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 *)