Fix function applications without labels (OCaml warning 6)

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

6 files changed, 24 insertions, 24 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 4f3369b698..7f5dacaaef 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -264,7 +264,7 @@ let add_new_coercion_core coef stre source target isid =
   check_arity cls;
   check_arity clt;
   let stre' = get_strength stre coef cls clt in
-  declare_coercion coef stre' isid cls clt (List.length lvs)
+  declare_coercion coef stre' ~isid ~src:cls ~target:clt ~params:(List.length lvs)
 
 let try_add_new_coercion_core ref b c d e =
   try add_new_coercion_core ref b c d e
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index dfb1b4ddc2..26a5cb36f6 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -50,9 +50,9 @@ let load_rcfile() =
     Flags.if_verbose msgnl (str"Skipping rcfile loading.")
 
 (* Puts dir in the path of ML and in the LoadPath *)
-let coq_add_path d s =
-  Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
-let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root])
+let coq_add_path unix_path s =
+  Mltop.add_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
+let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root])
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -92,21 +92,21 @@ let init_load_path () =
   let dirs = ["states";"plugins"] in
     (* first user-contrib *)
     if Sys.file_exists user_contrib then
-      Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
+      Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix;
     (* then states, theories and dev *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
     (* developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
     List.iter
-      (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
+      (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
       theories_dirs_map;
     (* then current directory *)
-    Mltop.add_path "." Nameops.default_root_prefix;
+    Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix;
     (* additional loadpath, given with -I -include -R options *)
     List.iter
-      (fun (s,alias,reci) ->
-	if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
+      (fun (unix_path, coq_root, reci) ->
+	if reci then Mltop.add_rec_path ~unix_path ~coq_root else Mltop.add_path ~unix_path ~coq_root)
       (List.rev !includes)
 
 let init_library_roots () =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 429d39e205..446efc9540 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -126,8 +126,8 @@ let add_ml_dir s =
     | _ -> ()
 
 (* For Rec Add ML Path *)
-let add_rec_ml_dir dir =
-  List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs dir)
+let add_rec_ml_dir unix_path =
+  List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path)
 
 (* Adding files to Coq and ML loadpath *)
 
@@ -148,19 +148,19 @@ let convert_string d =
     flush_all ();
     failwith "caught"
 
-let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
-  if exists_dir dir then
-    let dirs = all_subdirs dir in
-    let prefix = Names.repr_dirpath coq_dirpath in
+let add_rec_path ~unix_path ~coq_root =
+  if exists_dir unix_path then
+    let dirs = all_subdirs ~unix_path in
+    let prefix = Names.repr_dirpath coq_root in
     let convert_dirs (lp,cp) =
       (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
     let dirs = map_succeed convert_dirs dirs in
     List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
-    add_ml_dir dir;
+    add_ml_dir unix_path;
     List.iter (Library.add_load_path false) dirs;
-    Library.add_load_path true (dir,coq_dirpath)
+    Library.add_load_path true (unix_path, coq_root)
   else
-    msg_warning (str ("Cannot open " ^ dir))
+    msg_warning (str ("Cannot open " ^ unix_path))
 
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 1ef51496b1..b87d11d54f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -203,7 +203,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 	      Impargs.maybe_declare_manual_implicits false refi impls;
 	      if coe then begin
 	        let cl = Class.class_of_global (IndRef indsp) in
-	        Class.try_add_new_coercion_with_source refi Global cl
+	        Class.try_add_new_coercion_with_source refi Global ~source:cl
 	      end;
 	      let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 	      let constr_fip = applist (constr_fi,proj_args) in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index e01978dc14..b2e33d1d3b 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -191,7 +191,7 @@ let filter_by_module_from_list = function
   | l, outside -> filter_by_module l (not outside)
 
 let filter_subproof gr _ _ =
-  not (string_string_contains (name_of_reference gr) "_subproof")
+  not (string_string_contains ~where:(name_of_reference gr) ~what:"_subproof")
 
 let (&&&&&) f g x y z = f x y z && g x y z
 
@@ -216,7 +216,7 @@ type glob_search_about_item =
 
 let search_about_item (itemref,typ) = function
   | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
-  | GlobSearchString s -> string_string_contains (name_of_reference itemref) s
+  | GlobSearchString s -> string_string_contains ~where:(name_of_reference itemref) ~what:s
 
 let raw_search_about filter_modules display_function l =
   let filter ref' env typ =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b7524eea0d..f6fb8aa51d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -585,13 +585,13 @@ let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' stre source target;
+  Class.try_add_new_coercion_with_target ref' stre ~source ~target;
   if_verbose msgnl (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion stre id qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id stre source target
+  Class.try_add_new_identity_coercion id stre ~source ~target
 
 (* Type classes *)
 
@@ -694,7 +694,7 @@ let vernac_add_loadpath isrec pdir ldiropt =
   let alias = match ldiropt with
     | None -> Nameops.default_root_prefix
     | Some ldir -> ldir in
-  (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
+  (if isrec then Mltop.add_rec_path else Mltop.add_path) ~unix_path:pdir ~coq_root:alias
 
 let vernac_remove_loadpath path =
   Library.remove_load_path (System.expand_path_macros path)