fix a few more Ocaml 4.02 warnings

plugins/transform/hypothesis_selection.ml

@@ -48,9 +48,9 @@ module Sexpr = Set.Make(ExprNode)
 (** prints the given expression, transforming spaces into _ *)
 let string_of_expr_node node =
   let print_in_buf printer x =
-    let b = Buffer.create 42 in
-    Format.bprintf b "@[%a@]" printer x;
-    Buffer.contents b in
+    Format.fprintf Format.str_formatter "@[%a@]" printer x;
+    Format.flush_str_formatter()
+  in
   let white_space = Str.regexp "[ ()]" in
   let translate x = Str.global_replace white_space "_" x in
   let repr = print_in_buf Pretty.print_term node in
@@ -362,7 +362,7 @@ module Select = struct
       | Tnot f -> fmla_get_pred ~pos:false acc f
       | Tapp (pred,_) -> (pred, (if pos then `Positive else `Negative))::acc
       | _ -> failwith "bad formula in get_predicates !"
-    in List.fold_left fmla_get_pred acc clause
+    in List.fold_left (fmla_get_pred ?pos:None) acc clause
 
   (** get all sub-formulae *)
   let get_sub_fmlas fTbl tTbl fmla =
@@ -598,4 +598,3 @@ Local Variables:
 End:
 vim:foldmethod=indent:foldnestmax=1
 *)
-

src/driver/whyconf.ml

@@ -209,11 +209,11 @@ exception StepsCommandNotSpecified of string
 let get_complete_command pc stepslimit =
   let comm = if stepslimit < 0 then pc.command
     else
-      match pc.command_steps with 
+      match pc.command_steps with
       | None -> raise (StepsCommandNotSpecified "The solver is used with step limit and the command for running the solver with steplimit is not specified.")
       | Some command_steps -> command_steps in
   String.concat " " (comm :: pc.extra_options)
-    
+
 let set_limits m time mem running =
   { m with timelimit = time; memlimit = mem; running_provers_max = running }
 
@@ -281,8 +281,8 @@ exception NonUniqueId
 let set_prover _ (prover,shortcuts) family =
   let section = empty_section in
   let section = set_string section "name" prover.prover.prover_name in
-  let section = set_string section "command" prover.command in    
-  let section = 
+  let section = set_string section "command" prover.command in
+  let section =
     Opt.fold (fun s c -> set_string s "command_steps" c) section prover.command_steps
   in
   let section = set_string section "driver" prover.driver in
@@ -568,9 +568,8 @@ let read_config conf_file =
   try
     get_config filenamerc
   with e when not (Debug.test_flag Debug.stack_trace) ->
-    let b = Buffer.create 40 in
-    Format.bprintf b "%a" Exn_printer.exn_printer e;
-    raise (ConfigFailure (fst filenamerc, Buffer.contents b))
+    Format.fprintf str_formatter "%a" Exn_printer.exn_printer e;
+    raise (ConfigFailure (fst filenamerc, flush_str_formatter ()))
 
 (** filter prover *)
 type regexp_desc = { reg : Str.regexp; desc : string}

src/session/strategy_parser.mll

@@ -143,7 +143,7 @@ rule scan code = parse
   let parse env s =
     let code = create_code env in
     scan code (Lexing.from_string s);
-    let label = Array.create code.temp 0 in
+    let label = Array.make code.temp 0 in
     let fill name lab = match lab.defined with
       | None -> error "label '%s' is undefined" name
       | Some n -> label.(lab.temporary) <- n in

src/session/termcode.ml

@@ -266,9 +266,8 @@ let ident_shape ~push id acc =
   id_string_shape ~push id.Ident.id_string acc
 
 let const_shape ~push acc c =
-  let b = Buffer.create 17 in
-  Format.bprintf b "%a" Pretty.print_const c;
-  push (Buffer.contents b) acc
+  Format.fprintf Format.str_formatter "%a" Pretty.print_const c;
+  push (Format.flush_str_formatter ()) acc
 
 let rec pat_shape ~(push:string->'a->'a) c m (acc:'a) p : 'a =
   match p.pat_node with
@@ -442,12 +441,9 @@ module Checksum = struct
     | CV1 -> ident_v1 b id
     | CV2 -> ident_v2 b id
 
-  let const =
-    let buf = Buffer.create 17 in
-    fun b c ->
-      Format.bprintf buf "%a" Pretty.print_const c;
-      let s = Buffer.contents buf in
-      Buffer.clear buf;
+  let const b c =
+      Format.fprintf Format.str_formatter "%a" Pretty.print_const c;
+      let s = Format.flush_str_formatter () in
       string b s
 
   let tvsymbol b tv = ident b tv.Ty.tv_name

src/transform/eliminate_definition.ml

@@ -291,7 +291,7 @@ let bisect_step task0 =
     | Some {task_prev = t} -> length acc t
     | None -> acc in
   let n = length 0 task in
-  let a = Array.create n (Obj.magic 0) in
+  let a = Array.make n (Obj.magic 0) in
   let rec init acc = function
     | Some {task_decl = {td_node = Decl d}; task_prev = t} ->
       a.(acc) <- d; init (acc - 1) t

src/util/debug.ml

@@ -65,14 +65,10 @@ let time_start = Unix.gettimeofday ()
 
 let set_debug_formatter f =
   (** enable the usual behavior of stderr: flush at every new line *)
-  let out,flush,newline,spaces =
-    Format.pp_get_all_formatter_output_functions f () in
-  Format.pp_set_all_formatter_output_functions
-    f
-    ~out
-    ~flush
-    ~newline:(fun () -> newline (); flush ())
-    ~spaces;
+  let o = Format.pp_get_formatter_out_functions f () in
+  Format.pp_set_formatter_out_functions f
+    { o with Format.out_newline =
+        (fun () -> o.Format.out_newline (); o.Format.out_flush ()) };
   formatter := f
 
 let get_debug_formatter () = !formatter

src/util/pp.ml

@@ -176,10 +176,15 @@ let string_of ?max_boxes p x =
   Buffer.contents b
 
 let wnl fmt =
+(*
   let out,flush,_newline,spaces =
     pp_get_all_formatter_output_functions fmt () in
   pp_set_all_formatter_output_functions fmt
     ~out ~flush ~newline:(fun () -> spaces 1) ~spaces
+*)
+  let o = pp_get_formatter_out_functions fmt () in
+  pp_set_formatter_out_functions fmt
+    { o with out_newline = (fun () -> o.out_spaces 1) }
 
 
 let string_of_wnl p x =

src/whyml/mlw_module.ml

@@ -285,7 +285,7 @@ let add_decl uc d =
     | Decl.Dind (_,dl) -> List.fold_left add_logic uc dl
     | Decl.Dprop _ -> uc
   in
-  add_to_theory Theory.add_decl uc d
+  add_to_theory (Theory.add_decl ?warn:None) uc d
 
 let use_export_theory uc th =
   let nth = Theory.use_export uc.muc_theory th in