Fix omitted labels in function calls

33 files changed, 108 insertions, 106 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 1dd8da12a..b14fba975 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -129,7 +129,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let gl = mlexpr_of_clause clause in
   let level = mlexpr_of_int level in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in
+  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 222b9eed9..259557f40 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -117,7 +117,7 @@ end = struct
       (b#get_iter_at_mark s.start)#offset
       (b#get_iter_at_mark s.stop)#offset
       (ellipsize
-        ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
+        ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop)))
       (String.concat "," (List.map str_of_flag s.flags))
       (ellipsize
         (String.concat ","
@@ -207,7 +207,7 @@ object (self)
     in
     List.iter (fun s -> set_index s (s.index + 1)) after;
     set_index s (document_length - List.length after);
-    ignore ((SentenceId.connect s)#changed self#on_changed);
+    ignore ((SentenceId.connect s)#changed ~callback:self#on_changed);
     document_length <- document_length + 1;
     List.iter (fun f -> f `INSERT) cbs
 
@@ -221,8 +221,8 @@ object (self)
     List.iter (fun f -> f `REMOVE) cbs
 
   initializer
-    let _ = (Doc.connect doc)#pushed self#on_push in
-    let _ = (Doc.connect doc)#popped self#on_pop in
+    let _ = (Doc.connect doc)#pushed ~callback:self#on_push in
+    let _ = (Doc.connect doc)#popped ~callback:self#on_pop in
     ()
 
 end
@@ -273,15 +273,15 @@ object(self)
         else iter
       in
       let iter = sentence_start iter in
-      script#buffer#place_cursor iter;
+      script#buffer#place_cursor ~where:iter;
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
-    let _ = segment#connect#clicked on_click in
+    let _ = segment#connect#clicked ~callback:on_click in
     ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
-    let x, y = script#window_to_buffer_coords `WIDGET x y in
-    let iter = script#get_iter_at_location x y in
+    let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+    let iter = script#get_iter_at_location ~x ~y in
     if iter#has_tag Tags.Script.tooltip then begin
       let s =
         let rec aux iter =
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 25858acce..0b7567a5a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -792,11 +792,11 @@ let coqtop_arguments sn =
         sn.messages#push Feedback.Error (Pp.str msg)
     else dialog#destroy ()
   in
-  let _ = entry#connect#activate ok_cb in
-  let _ = ok#connect#clicked ok_cb in
+  let _ = entry#connect#activate ~callback:ok_cb in
+  let _ = ok#connect#clicked ~callback:ok_cb in
   let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in
   let cancel_cb () = dialog#destroy () in
-  let _ = cancel#connect#clicked cancel_cb in
+  let _ = cancel#connect#clicked ~callback:cancel_cb in
   dialog#show ()
 
 let coqtop_arguments = cb_on_current_term coqtop_arguments
@@ -1274,8 +1274,8 @@ let build_ui () =
     if b then toolbar#misc#show () else toolbar#misc#hide ()
   in
   stick show_toolbar toolbar refresh_toolbar;
-  let _ = source_style#connect#changed refresh_style in
-  let _ = source_language#connect#changed refresh_language in
+  let _ = source_style#connect#changed ~callback:refresh_style in
+  let _ = source_language#connect#changed ~callback:refresh_language in
 
   (* Color configuration *)
   Tags.Script.incomplete#set_property
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bf86db08f..ca0ef38d3 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -82,7 +82,7 @@ let add ((s,eid),(sid,verbose)) =
   let loc_ast = Stm.parse_sentence sid pa in
   let newid, rc = Stm.add ~ontop:sid verbose loc_ast in
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  ide_cmd_checks newid loc_ast;
+  ide_cmd_checks ~id:newid loc_ast;
   (* TODO: the "" parameter is a leftover of the times the protocol
    * used to include stderr/stdout output.
    *
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index da867e689..d7d38a5ec 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -58,7 +58,7 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
     let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in
     let start = buf#get_iter_at_mark mark in
     let stop = buf#get_iter_at_mark rmark in
-    let iter tag = buf#apply_tag tag start stop in
+    let iter tag = buf#apply_tag tag ~start ~stop in
     List.iter iter tags
 
 let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
diff --git a/ide/preferences.ml b/ide/preferences.ml
index f0fd45d77..e1fc4005b 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -73,8 +73,8 @@ end
 let stick (pref : 'a preference) (obj : #GObj.widget as 'obj)
   (cb : 'a -> unit) =
   let _ = cb pref#get in
-  let p_id = pref#connect#changed (fun v -> cb v) in
-  let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in
+  let p_id = pref#connect#changed ~callback:(fun v -> cb v) in
+  let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
   ()
 
 (** Useful marshallers *)
@@ -314,7 +314,7 @@ let attach_modifiers (pref : string preference) prefix =
     in
     GtkData.AccelMap.foreach change
   in
-  pref#connect#changed cb
+  pref#connect#changed ~callback:cb
 
 let modifier_for_navigation =
   new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)
@@ -408,10 +408,10 @@ let background_color =
   new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)
 
 let attach_bg (pref : string preference) (tag : GText.tag) =
-  pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c))
+  pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c))
 
 let attach_fg (pref : string preference) (tag : GText.tag) =
-  pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c))
+  pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c))
 
 let processing_color =
   new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
@@ -468,7 +468,7 @@ let create_tag name default =
   let iter table =
     let tag = GText.tag ~name () in
     table#add tag#as_tag;
-    ignore (pref#connect#changed (fun _ -> set_tag tag));
+    ignore (pref#connect#changed ~callback:(fun _ -> set_tag tag));
     set_tag tag;
   in
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
@@ -601,8 +601,8 @@ object (self)
     box#pack italic#coerce;
     box#pack underline#coerce;
     let cb but obj = obj#set_sensitive (not but#active) in
-    let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in
-    let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in
+    let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
+    let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
     ()
 
 end
@@ -692,7 +692,7 @@ let configure ?(apply=(fun () -> ())) () =
         ~color:(Tags.color_of_string pref#get)
         ~packing:(table#attach ~left:1 ~top:i) ()
       in
-      let _ = button#connect#color_set begin fun () ->
+      let _ = button#connect#color_set ~callback:begin fun () ->
         pref#set (Tags.string_of_color button#color)
       end in
       let reset _ =
@@ -754,7 +754,7 @@ let configure ?(apply=(fun () -> ())) () =
     let button text (pref : bool preference) =
       let active = pref#get in
       let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
-      ignore (but#connect#toggled (fun () -> pref#set but#active))
+      ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active))
     in
     let () = button "Dynamic word wrap" dynamic_word_wrap in
     let () = button "Show line number" show_line_number in
diff --git a/ide/session.ml b/ide/session.ml
index 6262820e7..7aea75ac8 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -249,8 +249,8 @@ let make_table_widget ?sort cd cb =
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true in
   let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed refresh in
-  let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in
+  let _ = background_color#connect#changed ~callback:refresh in
+  let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -308,8 +308,8 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
         !callback errs;
 	List.iter (fun (lno, msg) -> access (fun columns store ->
           let line = store#append () in
-          store#set line (find_int_col "Line" columns) lno;
-          store#set line (find_string_col "Error message" columns) msg))
+          store#set ~row:line ~column:(find_int_col "Line" columns) lno;
+          store#set ~row:line ~column:(find_string_col "Error message" columns) msg))
           errs
       end
     method on_update ~callback:cb = callback := cb
@@ -348,8 +348,8 @@ let create_jobpage coqtop coqops : jobpage =
               else false)
           else
             let line = store#append () in
-            store#set line column id;
-            store#set line (find_string_col "Job name" columns) job))
+            store#set ~row:line ~column id;
+            store#set ~row:line ~column:(find_string_col "Job name" columns) job))
           jobs
       end
     method on_update ~callback:cb = callback := cb
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 3fcb7ce49..621c46b94 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -91,8 +91,8 @@ object(self)
     let result = GText.view ~packing:r_bin#add () in
     views <- (frame#coerce, result, combo#entry) :: views;
     let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
-    let _ = background_color#connect#changed cb in
-    let _ = result#misc#connect#realize (fun () -> cb background_color#get) in
+    let _ = background_color#connect#changed ~callback:cb in
+    let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
     let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
     stick text_font result cb;
     result#misc#set_can_focus true; (* false causes problems for selection *)
@@ -165,7 +165,7 @@ object(self)
     self#new_page_maker;
     self#new_query_aux ~grab_now:false ();
     frame#misc#hide ();
-    let _ = background_color#connect#changed self#refresh_color in
+    let _ = background_color#connect#changed ~callback:self#refresh_color in
     self#refresh_color background_color#get;
     ignore(notebook#event#connect#key_press ~callback:(fun ev ->
       if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true)
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index aeae3e1fd..3bb6b780e 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -154,7 +154,7 @@ object (self)
     let () = store#clear () in
     let iter prop =
       let iter = store#append () in
-      store#set iter column prop
+      store#set ~row:iter ~column prop
     in
     let () = current_completion <- (pref, props) in
     Proposals.iter iter props
@@ -267,7 +267,7 @@ object (self)
     (** Position of view w.r.t. window *)
     let (ux, uy) = Gdk.Window.get_position view#misc#window in
     (** Relative buffer position to view *)
-    let (dx, dy) = view#window_to_buffer_coords `WIDGET 0 0 in
+    let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in
     (** Iter position *)
     let iter = view#buffer#get_iter pos in
     let coords = view#get_iter_location iter in
@@ -397,11 +397,11 @@ object (self)
     let () = self#select_first () in
     let () = obj#misc#show () in
     let () = self#manage_scrollbar () in
-    obj#resize 1 1
+    obj#resize ~width:1 ~height:1
 
   method private start_callback off =
     let (x, y, w, h) = self#coordinates (`OFFSET off) in
-    let () = obj#move x (y + 3 * h / 2) in
+    let () = obj#move ~x ~y:(y + 3 * h / 2) in
     ()
 
   method private update_callback (off, word, props) =
@@ -433,21 +433,21 @@ object (self)
       else false
     in
     (** Style handling *)
-    let _ = view#misc#connect#style_set self#refresh_style in
+    let _ = view#misc#connect#style_set ~callback:self#refresh_style in
     let _ = self#refresh_style () in
     let _ = data#set_resize_mode `PARENT in
     let _ = frame#set_resize_mode `PARENT in
     (** Callback to model *)
-    let _ = model#connect#start_completion self#start_callback in
-    let _ = model#connect#update_completion self#update_callback in
-    let _ = model#connect#end_completion self#end_callback in
+    let _ = model#connect#start_completion ~callback:self#start_callback in
+    let _ = model#connect#update_completion ~callback:self#update_callback in
+    let _ = model#connect#end_completion ~callback:self#end_callback in
     (** Popup interaction *)
-    let _ = view#event#connect#key_press key_cb in
+    let _ = view#event#connect#key_press ~callback:key_cb in
     (** Hiding the popup when necessary*)
-    let _ = view#misc#connect#hide obj#misc#hide in
-    let _ = view#event#connect#button_press (fun _ -> self#hide (); false) in
-    let _ = view#connect#move_cursor move_cb in
-    let _ = view#event#connect#focus_out (fun _ -> self#hide (); false) in
+    let _ = view#misc#connect#hide ~callback:obj#misc#hide in
+    let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in
+    let _ = view#connect#move_cursor ~callback:move_cb in
+    let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in
     ()
 
 end
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 3d847ddcc..f84b9063b 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -186,8 +186,8 @@ class finder name (view : GText.view) =
       in
       let find_cb = generic_cb self#hide self#find_forward in
       let replace_cb = generic_cb self#hide self#replace in
-      let _ = find_entry#event#connect#key_press find_cb in
-      let _ = replace_entry#event#connect#key_press replace_cb in
+      let _ = find_entry#event#connect#key_press ~callback:find_cb in
+      let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
 
       (** TextView interaction *)
       let view_cb ev =
@@ -197,7 +197,7 @@ class finder name (view : GText.view) =
           else false
         else false
       in
-      let _ = view#event#connect#key_press view_cb in
+      let _ = view#event#connect#key_press ~callback:view_cb in
       ()
 
   end
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 3cbe58388..f801091cf 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -188,8 +188,8 @@ let proof_view () =
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed cb in
-  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let _ = background_color#connect#changed ~callback:cb in
+  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
 
@@ -226,5 +226,5 @@ let proof_view () =
   (* Is there a better way to connect the signal ? *)
   (* Can this be done in the object constructor? *)
   let w_cb _ = pf#refresh ~force:false in
-  ignore (view#misc#connect#size_allocate w_cb);
+  ignore (view#misc#connect#size_allocate ~callback:w_cb);
   pf
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 218cedb36..7c058febd 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -460,8 +460,8 @@ object (self)
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
     (** Plug on preferences *)
     let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
-    let _ = background_color#connect#changed cb in
-    let _ = self#misc#connect#realize (fun () -> cb background_color#get) in
+    let _ = background_color#connect#changed ~callback:cb in
+    let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
 
     let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in
     stick dynamic_word_wrap self cb;
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index dbc1740ef..d527a0d13 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -75,7 +75,7 @@ object (self)
         self#redraw ();
       end
     in
-    let _ = box#misc#connect#size_allocate cb in
+    let _ = box#misc#connect#size_allocate ~callback:cb in
     let clicked_cb ev = match model with
     | None -> true
     | Some md ->
@@ -86,7 +86,7 @@ object (self)
       let () = clicked#call idx in
       true
     in
-    let _ = eventbox#event#connect#button_press clicked_cb in
+    let _ = eventbox#event#connect#button_press ~callback:clicked_cb in
     let cb show = if show then self#misc#show () else self#misc#hide () in
     stick show_progress_bar self cb;
     (** Initial pixmap *)
@@ -102,7 +102,7 @@ object (self)
     | `SET (i, color) ->
       if self#misc#visible then self#fill_range color i (i + 1)
     in
-    md#changed changed_cb
+    md#changed ~callback:changed_cb
 
   method private fill_range color i j = match model with
   | None -> ()
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cd975ee9a..ba714ada2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -487,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
         if eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_instances false u1 u2 cuniv in
+	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
              convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
 	if Int.equal j1 j2 && eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_instances false u1 u2 cuniv in
+	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 	  
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 6a28d1e00..71e02b3ba 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -82,7 +82,7 @@ let set_all_warnings_status status =
 
 let set_category_status ~name status =
   let names = Hashtbl.find categories name in
-  List.iter (fun name -> set_warning_status name status) names
+  List.iter (fun name -> set_warning_status ~name status) names
 
 let is_all_keyword name = CString.equal name "all"
 let is_none_keyword s = CString.equal s "none"
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 6d259e1b1..f25b394f0 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -345,13 +345,13 @@ let rec string loc ~comm_level bp len = parser
       if esc then string loc ~comm_level bp (store len '"') s else (loc, len)
   | [< ''('; s >] ->
       (parser
-        | [< ''*'; s >] ->
-            string loc
-              (Option.map succ comm_level)
+      | [< ''*'; s >] ->
+        let comm_level = Option.map succ comm_level in
+            string loc ~comm_level
               bp (store (store len '(') '*')
               s
         | [< >] ->
-            string loc comm_level bp (store len '(') s) s
+            string loc ~comm_level bp (store len '(') s) s
   | [< ''*'; s >] ->
       (parser
         | [< '')'; s >] ->
@@ -361,9 +361,9 @@ let rec string loc ~comm_level bp len = parser
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in
-            string loc comm_level bp (store (store len '*') ')') s
+            string loc ~comm_level bp (store (store len '*') ')') s
         | [< >] ->
-            string loc comm_level bp (store len '*') s) s
+            string loc ~comm_level bp (store len '*') s) s
   | [< ''\n' as c; s >] ep ->
      (* If we are parsing a comment, the string if not part of a token so we
      update the first line of the location. Otherwise, we update the last
@@ -372,8 +372,8 @@ let rec string loc ~comm_level bp len = parser
        if Option.has_some comm_level then bump_loc_line loc ep
        else bump_loc_line_last loc ep
      in
-     string loc comm_level bp (store len c) s
-  | [< 'c; s >] -> string loc comm_level bp (store len c) s
+     string loc ~comm_level bp (store len c) s
+  | [< 'c; s >] -> string loc ~comm_level bp (store len c) s
   | [< _ = Stream.empty >] ep ->
      let loc = set_loc_pos loc bp ep in
      err loc Unterminated_string
@@ -613,7 +613,7 @@ let rec next_token loc = parser bp
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       comment_stop bp;
       (INT (get_buff len), set_loc_pos loc bp ep)
-  | [< ''\"'; (loc,len) = string loc None bp 0 >] ep ->
+  | [< ''\"'; (loc,len) = string loc ~comm_level:None bp 0 >] ep ->
       comment_stop bp;
       (STRING (get_buff len), set_loc_pos loc bp ep)
   | [< ' ('(' as c);
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2b12462ad..322fbcea7 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -657,7 +657,7 @@ let extraction_library is_rec m =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, extract_structure env mp no_delta true struc) :: l
+    then (mp, extract_structure env mp no_delta ~all:true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cd8c9e471..8cda73b4b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -320,7 +320,7 @@ let add_tactic_notation local n prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local n prods false ids tac
+  add_glob_tactic_notation local ~level:n prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f3555ebc4..fc7963b2d 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1261,7 +1261,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in
     let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in
     let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in
-    let concl = find_T env0 concl0 1 do_subst in
+    let concl = find_T env0 concl0 1 ~k:do_subst in
     let _ = end_T () in
     concl
   | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) ->
@@ -1273,11 +1273,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     (* we start from sigma, so hole is considered a rigid head *)
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in
-    let concl = find_T env0 concl0 1 (fun env c _ h ->
+    let concl = find_T env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
       fs p_sigma (find_X env (fs sigma p) h 
-        (fun env _ -> do_subst env e_body))) in
+        ~k:(fun env _ -> do_subst env e_body))) in
     let _ = end_X () in let _ = end_T () in 
     concl
   | Some (sigma, E_In_X_In_T (e, hole, p)) ->
@@ -1289,11 +1289,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_X, end_X = mk_tpattern_matcher sigma noindex holep in
     let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in
     let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in
-    let concl = find_T env0 concl0 1 (fun env c _ h ->
+    let concl = find_T env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
-        find_E env e_body h do_subst))) in
+      fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h ->
+        find_E env e_body h ~k:do_subst))) in
     let _ = end_E () in let _ = end_X () in let _ = end_T () in
     concl
   | Some (sigma, E_As_X_In_T (e, hole, p)) ->
@@ -1306,10 +1306,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher sigma occ holep in
-    let concl = find_TE env0 concl0 1 (fun env c _ h ->
+    let concl = find_TE env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
+      fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h ->
         let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in
         let e_body = fs e_sigma e in
         do_subst env e_body e_body h))) in
@@ -1352,7 +1352,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let ise, u = mk_tpattern env sigma0 (ise,EConstr.Unsafe.to_constr t) ok L2R p in
  let find_U, end_U =
    mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
- let concl = find_U env concl h (fun _ _ _ -> mkRel) in
+ let concl = find_U env concl h ~k:(fun _ _ _ -> mkRel) in
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae87cd8c0..497bde340 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -195,7 +195,7 @@ let _ =
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd (loc,s) =
   let names, _ = Global.global_universe_names () in
-    if CString.string_contains s "." then
+    if CString.string_contains ~where:s ~what:"." then
       match List.rev (CString.split '.' s) with
       | [] -> anomaly (str"Invalid universe name " ++ str s)
       | n :: dp -> 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 270320538..da3add2e5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1117,7 +1117,9 @@ let local_whd_state_gen flags sigma =
   whrec
 
 let raw_whd_state_gen flags env =
-  let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in
+  let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ())
+                         ~tactic_mode:false
+                         flags env sigma s) in
   f
 
 let stack_red_of_state_red f =
@@ -1127,7 +1129,7 @@ let stack_red_of_state_red f =
 (* Drops the Cst_stack *)
 let iterate_whd_gen refold flags env sigma s =
   let rec aux t =
-  let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
+  let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in
   let whd_sk = Stack.map aux sk in
   Stack.zip sigma ~refold (hd,whd_sk)
   in aux s
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0fe5c73f1..cb3538422 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -43,7 +43,7 @@ let cbv_native env sigma c =
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
   in
   Reductionops.Stack.zip ~refold:true sigma state
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e823373f7..3738aa94a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1380,7 +1380,7 @@ end = struct (* {{{ *)
       if not drop then begin
         let checked_proof = Future.chain ~pure:false future_proof (fun p ->
           let pobject, _ =
-            Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+            Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
           stm_vernac_interp stop
@@ -2432,7 +2432,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       let id = VCS.new_node ?id () in
       VCS.merge id ~ours:(Qed (qed None)) brname;
       VCS.delete_branch brname;
-      VCS.propagate_sideff None;
+      VCS.propagate_sideff ~replay:None;
       `Ok
   | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
       let ofp =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 54e4405d1..c430e776a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -357,12 +357,12 @@ let shelve_dependencies gls =
 
 let hintmap_of sigma hdc secvars concl =
   match hdc with
-  | None -> fun db -> Hint_db.map_none secvars db
+  | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
      fun db ->
      if Hint_db.use_dn db then (* Using dnet *)
-       Hint_db.map_eauto sigma secvars hdc concl db
-     else Hint_db.map_existential sigma secvars hdc concl db
+       Hint_db.map_eauto sigma ~secvars hdc concl db
+     else Hint_db.map_existential sigma ~secvars hdc concl db
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index bcc068d3d..240178c9a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1435,7 +1435,7 @@ let pr_hints_db (name,db,hintlist) =
 let pr_hint_list_for_head c =
   let dbs = current_db () in
   let validate (name, db) =
-    let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
+    let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
     (name, db, hints)
   in
   let valid_dbs = List.map validate dbs in
diff --git a/tools/coqc.ml b/tools/coqc.ml
index b12d48710..552a943c8 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -77,12 +77,12 @@ let parse_args () =
     | ("-v"|"--version") :: _ -> Usage.version 0
 
     | ("-where") :: _ ->
-        Envars.set_coqlib (fun x -> x);
+        Envars.set_coqlib ~fail:(fun x -> x);
         print_endline (Envars.coqlib ());
         exit 0
 
     | ("-config" | "--config") :: _ ->
-        Envars.set_coqlib (fun x -> x);
+        Envars.set_coqlib ~fail:(fun x -> x);
         Usage.print_config ();
         exit 0
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a9f1b7376..1c1c1be6a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -502,7 +502,7 @@ let coqdep () =
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
-      (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x)));
+      (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9cf075065..c3a755860 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -292,7 +292,7 @@ let init_gc () =
     between coqtop and coqc. *)
 
 let usage () =
-  Envars.set_coqlib CErrors.error;
+  Envars.set_coqlib ~fail:CErrors.error;
   init_load_path ();
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
@@ -609,7 +609,7 @@ let init_toplevel arglist =
       (* If we have been spawned by the Spawn module, this has to be done
        * early since the master waits us to connect back *)
       Spawned.init_channels ();
-      Envars.set_coqlib CErrors.error;
+      Envars.set_coqlib ~fail:CErrors.error;
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
       if !print_config then (Usage.print_config (); exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9ff320ee8..48cd70f69 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -125,7 +125,7 @@ let rec interp_vernac sid (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
-      let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
+      let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
       if ntip <> `NewTip then
diff --git a/vernac/class.ml b/vernac/class.ml
index 95114ec39..104f3c1db 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -311,7 +311,7 @@ let add_coercion_hook poly local ref =
   | Global -> false
   | Discharge -> assert false
   in
-  let () = try_add_new_coercion ref stre poly in
+  let () = try_add_new_coercion ref ~local:stre poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
@@ -324,6 +324,6 @@ let add_subclass_hook poly local ref =
   | Discharge -> assert false
   in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl stre poly
+  try_add_new_coercion_subclass cl ~local:stre poly
 
 let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)
diff --git a/vernac/command.ml b/vernac/command.ml
index b27d8a0a3..b2f5755ce 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -258,7 +258,7 @@ match local with
   let () = Universes.register_universe_binders gr pl in
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
-  let () = if is_coe then Class.try_add_new_coercion gr local p in
+  let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = 
     if p (* polymorphic *) then Univ.UContext.instance ctx 
     else Univ.Instance.empty
@@ -752,7 +752,7 @@ let do_mutual_inductive indl poly prv finite =
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194..c6588684a 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -151,7 +151,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
   const, Safe_typing.add_private
-     (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff
+     (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -172,7 +172,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
   consts,
   Safe_typing.add_private 
     (Safe_typing.private_con_of_scheme
-      kind (Global.safe_env()) (Array.to_list schemes))
+      ~kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
 let define_mutual_scheme kind mode names mind =
@@ -185,7 +185,7 @@ let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
   s, Safe_typing.add_private
       (Safe_typing.private_con_of_scheme
-            kind (Global.safe_env()) [ind, s])
+            ~kind (Global.safe_env()) [ind, s])
       Safe_typing.empty_private_constants
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f805eeaa9..f86a0ef92 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1196,7 +1196,7 @@ let inNotation : notation_obj -> obj =
 (**********************************************************************)
 
 let with_lib_stk_protection f x =
-  let fs = Lib.freeze `No in
+  let fs = Lib.freeze ~marshallable:`No in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
     let reraise = CErrors.push reraise in