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

16 files changed, 120 insertions, 120 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 570220981d..3dc510dccf 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -273,7 +273,7 @@ let with_magic_number_check f a =
 let mk_library md f get_table digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = Safe_typing.LightenLibrary.load true get_table md.md_compiled;
+  library_compiled = Safe_typing.LightenLibrary.load ~load_proof:true get_table md.md_compiled;
   library_deps = md.md_deps;
   library_digest = digest }
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 9646141d06..e8cc52ecf9 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -72,17 +72,17 @@ 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 = 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 = repr_dirpath coq_root in
     let convert_dirs (lp,cp) =
       (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
     let dirs = map_succeed convert_dirs dirs in
     List.iter Check.add_load_path dirs;
-    Check.add_load_path (dir,coq_dirpath)
+    Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str ("Cannot open " ^ dir))
+    msg_warning (str ("Cannot open " ^ unix_path))
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -105,21 +105,21 @@ let init_load_path () =
   let plugins = coqlib/"plugins" in
   (* first user-contrib *)
   if Sys.file_exists user_contrib then
-    add_rec_path user_contrib Check.default_root_prefix;
+    add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then plugins *)
-  add_rec_path plugins (Names.make_dirpath [coq_root]);
+  add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]);
   (* then standard library *)
 (*  List.iter
     (fun (s,alias) ->
       add_rec_path (coqlib/s) ([alias; coq_root]))
     theories_dirs_map;*)
-  add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]);
+  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
   (* then current directory *)
-  add_path "." Check.default_root_prefix;
+  add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
   (* additional loadpath, given with -I -include -R options *)
   List.iter
-    (fun (s,alias,reci) ->
-      if reci then add_rec_path s alias else add_path s alias)
+    (fun (unix_path, coq_root, reci) ->
+      if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root)
     (List.rev !includes);
   includes := []
 
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 0d0cdfc2ed..a351107d91 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -142,6 +142,6 @@ object(self)
     self#frame#misc#show ()
 
   initializer
-    ignore (new_page_menu#connect#clicked self#new_command);
+    ignore (new_page_menu#connect#clicked ~callback:self#new_command);
    (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
 end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 45eddc84a0..375d3eec23 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -135,7 +135,7 @@ let build_session s =
                  else img#set_stock `YES) in
   let _ =
     eval_paned#misc#connect#size_allocate
-      (let old_paned_width = ref 2 in
+      ~callback:(let old_paned_width = ref 2 in
        let old_paned_height = ref 2 in
          (fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
             if !old_paned_width <> paned_width || !old_paned_height <> paned_height then (
@@ -336,8 +336,8 @@ let get_current_word () =
 	  let it = av#get_insert in
 	  let start = find_word_start it in
 	  let stop = find_word_end start in
-	    script#buffer#move_mark `SEL_BOUND start;
-	    script#buffer#move_mark `INSERT stop;
+	    script#buffer#move_mark `SEL_BOUND ~where:start;
+	    script#buffer#move_mark `INSERT ~where:stop;
 	    script#buffer#get_text ~slice:true ~start ~stop ()
       | _,Some t ->
  	  prerr_endline "Some selected";
@@ -563,7 +563,7 @@ object(self)
                 let s = try_convert (Buffer.contents b) in
                   input_buffer#set_text s;
                   self#update_stats;
-                  input_buffer#place_cursor input_buffer#start_iter;
+                  input_buffer#place_cursor ~where:input_buffer#start_iter;
                   input_buffer#set_modified false;
                   pop_info ();
                   flash_info "Buffer reverted";
@@ -763,7 +763,7 @@ object(self)
                    input_buffer#apply_tag Tags.Script.error
                      ~start:starti
                      ~stop:stopi;
-                   input_buffer#place_cursor starti)
+                   input_buffer#place_cursor ~where:starti)
         end
       end in
     try
@@ -813,7 +813,7 @@ object(self)
                   let completion = input_buffer#get_text ~start ~stop () in
                     ignore (input_buffer#delete_selection ());
                     ignore (input_buffer#insert_interactive completion);
-                    input_buffer#move_mark `SEL_BOUND (it())#backward_char;
+                    input_buffer#move_mark `SEL_BOUND ~where:(it())#backward_char;
                     true
           end else false
           else false
@@ -854,7 +854,7 @@ object(self)
         (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
          if (self#get_insert#compare) stop <= 0 then
            begin
-             b#place_cursor stop;
+             b#place_cursor ~where:stop;
              self#recenter_insert
            end;
          let ide_payload = { start = `MARK (b#create_mark start);
@@ -884,7 +884,7 @@ object(self)
           input_buffer#apply_tag
             (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
              if (self#get_insert#compare) stop <= 0 then
-               input_buffer#place_cursor stop;
+               input_buffer#place_cursor ~where:stop;
              let ide_payload = { start = `MARK (input_buffer#create_mark start);
                                  stop = `MARK (input_buffer#create_mark stop); } in
              Stack.push ide_payload cmd_stack;
@@ -1051,7 +1051,7 @@ object(self)
             input_buffer#move_mark
               ~where:start
               (`NAME "start_of_input");
-            input_buffer#place_cursor start;
+            input_buffer#place_cursor ~where:start;
             self#recenter_insert;
             self#show_goals;
             self#clear_message
@@ -1123,7 +1123,7 @@ object(self)
   method activate () = if not is_active then begin
     is_active <- true;
     act_id <- Some
-                (input_view#event#connect#key_press self#active_keypress_handler);
+                (input_view#event#connect#key_press ~callback:self#active_keypress_handler);
     prerr_endline "CONNECTED active : ";
     print_id (Option.get act_id);
     match
@@ -1164,8 +1164,8 @@ object(self)
          last_index <- not last_index;)
 
   method private electric_paren tag =
-    let oparen_code = Glib.Utf8.to_unichar "("  (ref 0) in
-    let cparen_code = Glib.Utf8.to_unichar ")"  (ref 0) in
+    let oparen_code = Glib.Utf8.to_unichar "("  ~pos:(ref 0) in
+    let cparen_code = Glib.Utf8.to_unichar ")"  ~pos:(ref 0) in
       ignore (input_buffer#connect#insert_text ~callback:
                 (fun it x ->
                    input_buffer#remove_tag
@@ -1211,7 +1211,7 @@ object(self)
                            if (it#compare self#get_start_of_input)<0
                            then GtkSignal.stop_emit ();
                            if String.length s > 1 then
-                             (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it)));
+                             (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor ~where:it)));
     ignore (input_buffer#connect#after#apply_tag
               ~callback:(fun tag ~start ~stop ->
                            if (start#compare self#get_start_of_input)>=0
@@ -1240,7 +1240,7 @@ object(self)
                                  ((input_view#buffer#get_iter `SEL_BOUND)#offset)
                              in
                                if has_completed then
-                                 input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char;
+                                 input_buffer#move_mark `SEL_BOUND ~where:(input_buffer#get_iter `SEL_BOUND)#forward_char;
 
 
               )
@@ -1282,7 +1282,7 @@ object(self)
                                | None -> () )
       );
       ignore (input_buffer#connect#insert_text
-                (fun it s ->
+                ~callback:(fun it s ->
                    prerr_endline "Should recenter ?";
                    if String.contains s '\n' then begin
                                             prerr_endline "Should recenter : yes";
@@ -1602,7 +1602,7 @@ let main files =
           let input_buffer = session.script#buffer in
           prerr_endline "Loading: fill buffer";
           input_buffer#set_text s;
-          input_buffer#place_cursor input_buffer#start_iter;
+          input_buffer#place_cursor ~where:input_buffer#start_iter;
           prerr_endline ("Loading: switch to view "^ string_of_int index);
           session_notebook#goto_page index;
           prerr_endline "Loading: highlight";
@@ -1622,7 +1622,7 @@ let main files =
         | None -> ()
         | Some f -> load f
     in
-    ignore (load_m#connect#activate (load_f));
+    ignore (load_m#connect#activate ~callback:(load_f));
 
     let load_m = file_factory#add_item "_Open"
                    ~key:GdkKeysyms._O in
@@ -1631,7 +1631,7 @@ let main files =
         | None -> ()
         | Some f -> load f
     in
-    ignore (load_m#connect#activate (load_f));
+    ignore (load_m#connect#activate ~callback:(load_f));
 
     (* File/Save Menu *)
     let save_m = file_factory#add_item "_Save"
@@ -1660,7 +1660,7 @@ let main files =
       with
         | e -> warning "Save: unexpected error"
     in
-    ignore (save_m#connect#activate save_f);
+    ignore (save_m#connect#activate ~callback:save_f);
 
     (* File/Save As Menu *)
     let saveas_m = file_factory#add_item "S_ave as"
@@ -1694,7 +1694,7 @@ let main files =
                  end);
       with e -> flash_info "Save Failed"
     in
-    ignore (saveas_m#connect#activate saveas_f);
+    ignore (saveas_m#connect#activate ~callback:saveas_f);
     (* XXX *)
     (* File/Save All Menu *)
     let saveall_m = file_factory#add_item "Sa_ve all" in
@@ -1717,7 +1717,7 @@ let main files =
         )
         session_notebook#pages
     in
-    ignore (saveall_m#connect#activate saveall_f);
+    ignore (saveall_m#connect#activate ~callback:saveall_f);
     (* XXX *)
     (* File/Revert Menu *)
     let revert_m = file_factory#add_item "_Revert all buffers" in
@@ -1732,12 +1732,12 @@ let main files =
                     | _ -> ()
                 with _ -> av#revert)
     in
-    ignore (revert_m#connect#activate (fun () -> List.iter revert_f session_notebook#pages));
+    ignore (revert_m#connect#activate ~callback:(fun () -> List.iter revert_f session_notebook#pages));
 
     (* File/Close Menu *)
     let close_m =
       file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in
-    ignore (close_m#connect#activate remove_current_view_page);
+    ignore (close_m#connect#activate ~callback:remove_current_view_page);
 
     (* File/Print Menu *)
     let _ = file_factory#add_item "_Print..."
@@ -1792,7 +1792,7 @@ let main files =
     (* File/Rehighlight Menu *)
     let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
     ignore (rehighlight_m#connect#activate
-              (fun () ->
+              ~callback:(fun () ->
                  force_retag
                    session_notebook#current_term.script#buffer;
                  session_notebook#current_term.analyzed_view#recenter_insert));
@@ -1846,7 +1846,7 @@ let main files =
       let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
                 ~callback:quit_f
       in
-      ignore (w#event#connect#delete (fun _ -> quit_f (); true));
+      ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true));
 
       (* Edit Menu *)
       let edit_menu = factory#add_submenu "_Edit" in
@@ -1875,17 +1875,17 @@ let main files =
       ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
                (fun () -> GtkSignal.emit_unit
                             (get_active_view_for_cp ())
-                            GtkText.View.S.cut_clipboard
+                            ~sgn:GtkText.View.S.cut_clipboard
                ));
       ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
                (fun () -> GtkSignal.emit_unit
                             (get_active_view_for_cp ())
-                            GtkText.View.S.copy_clipboard));
+                            ~sgn:GtkText.View.S.copy_clipboard));
       ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
                (fun () ->
                   try GtkSignal.emit_unit
                         session_notebook#current_term.script#as_view
-                        GtkText.View.S.paste_clipboard
+                        ~sgn:GtkText.View.S.paste_clipboard
                   with _ -> prerr_endline "EMIT PASTE FAILED"));
       ignore (edit_f#add_separator ());
 
@@ -2041,7 +2041,7 @@ let main files =
 			in
 			let close_find () =
 			  let (v,b,_,stop) = last_find () in
-			    b#place_cursor stop;
+			    b#place_cursor ~where:stop;
 			    find_w#misc#hide();
 			    v#coerce#misc#grab_focus()
 			in
@@ -2100,14 +2100,14 @@ let main files =
 			    ~key:GdkKeysyms._B
 			    ~callback:(find_f ~backward:true)
 			  in
-			  let _ = close_find_button#connect#clicked close_find in
-			  let _ = replace_button#connect#clicked do_replace in
-			  let _ = replace_find_button#connect#clicked do_replace_find in
-			  let _ = find_again_button#connect#clicked find_again_forward in
-			  let _ = find_again_backward_button#connect#clicked find_again_backward in
-			  let _ = find_entry#connect#changed do_find in
+			  let _ = close_find_button#connect#clicked ~callback:close_find in
+			  let _ = replace_button#connect#clicked ~callback:do_replace in
+			  let _ = replace_find_button#connect#clicked ~callback:do_replace_find in
+			  let _ = find_again_button#connect#clicked ~callback:find_again_forward in
+			  let _ = find_again_backward_button#connect#clicked ~callback:find_again_backward in
+			  let _ = find_entry#connect#changed ~callback:do_find in
 			  let _ = find_entry#event#connect#key_press ~callback:key_find in
-			  let _ = find_w#event#connect#delete (fun _ -> find_w#misc#hide(); true) in
+			  let _ = find_w#event#connect#delete ~callback:(fun _ -> find_w#misc#hide(); true) in
 			    (*
 			      let search_if = edit_f#add_item "Search _forward"
 			      ~key:GdkKeysyms._greater
@@ -2408,9 +2408,9 @@ let main files =
 					    if view#buffer#insert_interactive text then begin
 						let iter = view#buffer#get_iter_at_mark `INSERT in
 						  ignore (iter#nocopy#backward_chars offset);
-						  view#buffer#move_mark `INSERT iter;
+						  view#buffer#move_mark `INSERT ~where:iter;
 						  ignore (iter#nocopy#backward_chars len);
-						  view#buffer#move_mark `SEL_BOUND iter;
+						  view#buffer#move_mark `SEL_BOUND ~where:iter;
 					      end in
 					  ignore (templates_factory#add_item menu_text ~callback ?key)
 				      in
@@ -2461,7 +2461,7 @@ let cur_ct = session_notebook#current_term.toplvl in
                                                     if view#buffer#insert_interactive s then
                                                       let i = view#buffer#get_iter (`MARK m) in
                                                       let _ = i#nocopy#forward_chars 9 in
-                                                      view#buffer#place_cursor i;
+                                                      view#buffer#place_cursor ~where:i;
                                                       view#buffer#move_mark ~where:(i#backward_chars 3)
                                                         `SEL_BOUND
                                             with Not_found -> flash_info "Not an inductive type"
@@ -2684,7 +2684,7 @@ let cur_ct = session_notebook#current_term.toplvl in
 						  input_buffer#apply_tag Tags.Script.error
    						    ~start:starti
 						    ~stop:stopi;
-						  input_buffer#place_cursor starti;
+						  input_buffer#place_cursor ~where:starti;
 						  av#set_message error_msg;
 						  v.script#misc#grab_focus ()
 					    with Not_found ->
@@ -2830,7 +2830,7 @@ let cur_ct = session_notebook#current_term.toplvl in
 						prerr_endline "End Search";
 						memo_search ();
 						let v = session_notebook#current_term.script in
-						  v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
+						  v#buffer#move_mark `SEL_BOUND ~where:(v#buffer#get_iter_at_mark `INSERT);
 						  v#coerce#misc#grab_focus ();
 						  search_input#entry#set_text "";
 						  search_lbl#misc#hide ();
@@ -2840,7 +2840,7 @@ let cur_ct = session_notebook#current_term.toplvl in
 						prerr_endline "End Search(focus out)";
 						memo_search ();
 						let v = session_notebook#current_term.script in
-						  v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
+						  v#buffer#move_mark `SEL_BOUND ~where:(v#buffer#get_iter_at_mark `INSERT);
 						  search_input#entry#set_text "";
 						  search_lbl#misc#hide ();
 						  search_input#misc#hide ()
@@ -2907,7 +2907,7 @@ let cur_ct = session_notebook#current_term.toplvl in
 							       ready_to_wrap_search := false;
 							       flash_info "Search wrapped";
 							       v#buffer#place_cursor
-								 (if !search_forward then v#buffer#start_iter else
+								 ~where:(if !search_forward then v#buffer#start_iter else
 								      v#buffer#end_iter);
 							       search_f ()
 							     end else begin
@@ -2920,8 +2920,8 @@ let cur_ct = session_notebook#current_term.toplvl in
 							   prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
 							   prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
 
-							   v#buffer#move_mark `SEL_BOUND start;
-							   v#buffer#move_mark `INSERT stop;
+							   v#buffer#move_mark `SEL_BOUND ~where:start;
+							   v#buffer#move_mark `INSERT ~where:stop;
 							   prerr_endline "search: after moving marks";
 							   prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
 							   prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
@@ -2938,11 +2938,11 @@ let cur_ct = session_notebook#current_term.toplvl in
 									    prerr_endline "search_key_rel: Placing sel_bound";
 									    v#buffer#move_mark
 									      `SEL_BOUND
-									      (v#buffer#get_iter_at_mark `INSERT)
+									      ~where:(v#buffer#get_iter_at_mark `INSERT)
 									| Some mk -> let it = v#buffer#get_iter_at_mark
 									    (`MARK mk) in
 										       prerr_endline "search_key_rel: Placing cursor";
-									    v#buffer#place_cursor it;
+									    v#buffer#place_cursor ~where:it;
 									    start_of_search := None
 								     );
 								     search_input#entry#set_text "";
@@ -2950,7 +2950,7 @@ let cur_ct = session_notebook#current_term.toplvl in
 								 end;
 							       false
 							    ));
-						  ignore (search_input#entry#connect#changed search_f);
+						  ignore (search_input#entry#connect#changed ~callback:search_f);
 						    push_info "Ready";
                                                                  (* Location display *)
 						    let l = GMisc.label
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index bb2bebe519..39cf14d3af 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -9,12 +9,12 @@
 open Ideutils
 
 
-let underscore = Glib.Utf8.to_unichar "_" (ref 0)
-let arobase = Glib.Utf8.to_unichar "@" (ref 0)
-let prime = Glib.Utf8.to_unichar "'" (ref 0)
-let bn = Glib.Utf8.to_unichar "\n" (ref 0)
-let space = Glib.Utf8.to_unichar " " (ref 0)
-let tab = Glib.Utf8.to_unichar "\t" (ref 0)
+let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
+let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
+let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
+let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0)
+let space = Glib.Utf8.to_unichar " " ~pos:(ref 0)
+let tab = Glib.Utf8.to_unichar "\t" ~pos:(ref 0)
 
 
 (* TODO: avoid num and prime at the head of a word *)
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index e77996a8f5..c84887d1aa 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -71,7 +71,7 @@ let mode_tactic sel_cb (proof:GText.view) = function
       insert_goal cur_goal cur_goal_menu 1 goals_cnt;
       Util.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
       ignore(proof#buffer#place_cursor  
-        ((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)));
+        ~where:((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)));
       ignore(proof#scroll_to_mark `INSERT)
 
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index b8eb2754f8..319cf4e4d2 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -16,11 +16,11 @@ exception Forbidden
 let status = GMisc.statusbar ()
 
 let push_info,pop_info =
-  let status_context = status#new_context "Messages" in
+  let status_context = status#new_context ~name:"Messages" in
     (fun s -> ignore (status_context#push s)),status_context#pop
 
 let flash_info =
-  let flash_context = status#new_context "Flash" in
+  let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 3833acfada..fefb268259 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -320,17 +320,17 @@ class ['a] list_selection_box
       in
       let _ = dbg "list_selection_box: connecting wb_add" in
       (* connect the functions to the buttons *)
-      ignore (wb_add#connect#clicked f_add);
+      ignore (wb_add#connect#clicked ~callback:f_add);
       let _ = dbg "list_selection_box: connecting wb_remove" in
-      ignore (wb_remove#connect#clicked f_remove);
+      ignore (wb_remove#connect#clicked ~callback:f_remove);
       let _ = dbg "list_selection_box: connecting wb_up" in
-      ignore (wb_up#connect#clicked (fun () -> self#up_selected));
+      ignore (wb_up#connect#clicked ~callback:(fun () -> self#up_selected));
       (
        match f_edit_opt with
 	 None -> ()
        | Some f ->
 	   let _ = dbg "list_selection_box: connecting wb_edit" in
-	   ignore (wb_edit#connect#clicked (fun () -> self#edit_selected f))
+	   ignore (wb_edit#connect#clicked ~callback:(fun () -> self#edit_selected f))
       );
       (* connect the selection and deselection of items in the clist *)
       let f_select ~row ~column ~event =
@@ -350,9 +350,9 @@ class ['a] list_selection_box
       in
       (* connect the select and deselect events *)
       let _ = dbg "list_selection_box: connecting select_row" in
-      ignore(wlist#connect#select_row f_select);
+      ignore(wlist#connect#select_row ~callback:f_select);
       let _ = dbg "list_selection_box: connecting unselect_row" in
-      ignore(wlist#connect#unselect_row f_unselect);
+      ignore(wlist#connect#unselect_row ~callback:f_unselect);
 
       (* initialize the clist with the listref *)
       self#update !listref
@@ -488,9 +488,9 @@ class color_param_box param (tt:GData.tooltips) =
     in
     let wb_ok = dialog#ok_button in
     let wb_cancel = dialog#cancel_button in
-    let _ = dialog#connect#destroy GMain.Main.quit in
+    let _ = dialog#connect#destroy ~callback:GMain.Main.quit in
     let _ = wb_ok#connect#clicked
-	(fun () ->
+	~callback:(fun () ->
 (*	  let color = dialog#colorsel#color in
 	  let r = (Gdk.Color.red color) in
 	  let g = (Gdk.Color.green color)in
@@ -505,11 +505,11 @@ class color_param_box param (tt:GData.tooltips) =
 	  dialog#destroy ()
 	)
     in
-    let _ = wb_cancel#connect#clicked dialog#destroy in
+    let _ = wb_cancel#connect#clicked ~callback:dialog#destroy in
     GMain.Main.main ()
   in
   let _ =
-    if param.color_editable then ignore (wb#connect#clicked f_sel)
+    if param.color_editable then ignore (wb#connect#clicked ~callback:f_sel)
   in
 
   object (self)
@@ -525,7 +525,7 @@ class color_param_box param (tt:GData.tooltips) =
 	()
 
     initializer
-      ignore (we#connect#changed (fun () -> set_color we#text));
+      ignore (we#connect#changed ~callback:(fun () -> set_color we#text));
 
   end ;;
 
@@ -573,19 +573,19 @@ class font_param_box param (tt:GData.tooltips) =
     dialog#selection#set_font_name !v;
     let wb_ok = dialog#ok_button in
     let wb_cancel = dialog#cancel_button in
-    let _ = dialog#connect#destroy GMain.Main.quit in
+    let _ = dialog#connect#destroy ~callback:GMain.Main.quit in
     let _ = wb_ok#connect#clicked
-	(fun () ->
+	~callback:(fun () ->
 	  let font = dialog#selection#font_name in
 	  we#set_text font ;
 	  set_entry_font (Some font);
 	  dialog#destroy ()
 	)
     in
-    let _ = wb_cancel#connect#clicked dialog#destroy in
+    let _ = wb_cancel#connect#clicked ~callback:dialog#destroy in
     GMain.Main.main ()
   in
-  let _ = if param.font_editable then ignore (wb#connect#clicked f_sel) in
+  let _ = if param.font_editable then ignore (wb#connect#clicked ~callback:f_sel) in
 
   object (self)
     (** This method returns the main box ready to be packed. *)
@@ -730,7 +730,7 @@ class filename_param_box param (tt:GData.tooltips) =
   in
   let _ =
     if param.string_editable then
-      let _ = wb#connect#clicked f_click in
+      let _ = wb#connect#clicked ~callback:f_click in
       ()
     else
       ()
@@ -782,7 +782,7 @@ class hotkey_param_box param (tt:GData.tooltips) =
   in
   let _ =
     if param.hk_editable then
-      ignore (we#event#connect#key_press capture)
+      ignore (we#event#connect#key_press ~callback:capture)
     else
       ()
   in
@@ -811,7 +811,7 @@ class modifiers_param_box param =
                                   ~active:(List.mem modifier param.md_value)
                                   ~packing:(hbox#pack ~expand:false) () in
                       ignore (but#connect#toggled
-                                (fun _ -> if but#active then value := modifier::!value
+                                ~callback:(fun _ -> if but#active then value := modifier::!value
                                  else value := List.filter ((<>) modifier) !value)))
             param.md_allow
   in
@@ -867,7 +867,7 @@ class date_param_box param (tt:GData.tooltips) =
   in
   let _ =
     if param.date_editable then
-      let _ = wb#connect#clicked f_click in
+      let _ = wb#connect#clicked ~callback:f_click in
       ()
     else
       ()
@@ -1102,9 +1102,9 @@ let edit ?(with_apply=true)
 	  | _ -> destroy (); rep
       with
 	  Failure s ->
-	    GToolbox.message_box "Error" s; iter rep
+	    GToolbox.message_box ~title:"Error" s; iter rep
 	| e ->
-	    GToolbox.message_box "Error" (Printexc.to_string e); iter rep
+	    GToolbox.message_box ~title:"Error" (Printexc.to_string e); iter rep
     in
       iter Return_cancel
 
@@ -1205,9 +1205,9 @@ let simple_edit ?(with_apply=true)
       | _ -> destroy (); rep
     with
       Failure s ->
-	GToolbox.message_box "Error" s; iter rep
+	GToolbox.message_box ~title:"Error" s; iter rep
     | e ->
-	GToolbox.message_box "Error" (Printexc.to_string e); iter rep
+	GToolbox.message_box ~title:"Error" (Printexc.to_string e); iter rep
   in
   iter Return_cancel
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 18f1d13ea6..6022e10070 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -208,7 +208,7 @@ let same c d = try check_same_type c d; true with _ -> false
 let has_curly_brackets ntn =
   String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
     String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
-    string_string_contains ntn " { _ } ")
+    string_string_contains ~where:ntn ~what:" { _ } ")
 
 let rec wildcards ntn n =
   if n = String.length ntn then []
diff --git a/library/library.ml b/library/library.ml
index 45d5c8f588..3d72c5fdb1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -384,7 +384,7 @@ let try_locate_qualified_library (loc,qid) =
 
 let mk_library md get_table digest = 
   let md_compiled = 
-    LightenLibrary.load !Flags.load_proofs get_table md.md_compiled
+    LightenLibrary.load ~load_proof:!Flags.load_proofs get_table md.md_compiled
   in {
     library_name     = md.md_name;
     library_compiled = md_compiled;
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)