diff --git a/src/core/ident.ml b/src/core/ident.ml
index b563e11a9290521878a85f1f6549bbc516faf2c8..cf6078e5ee199146139a8fdf8767c25f242ef091 100644
--- a/src/core/ident.ml
+++ b/src/core/ident.ml
@@ -45,7 +45,7 @@ let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag
 (* functions for working with counterexample model labels *)
 
 let is_model_trace_label label =
-  Lexlib.has_prefix "model_trace:" label.lab_string
+  Strings.has_prefix "model_trace:" label.lab_string
 
 let get_model_trace_label ~labels =
   Slab.choose (Slab.filter is_model_trace_label labels)
@@ -60,7 +60,7 @@ let transform_model_trace_label labels trans_fun =
 
 let append_to_model_element_name ~labels ~to_append =
   let trans lab_str =
-    let splitted = Str.bounded_split (Str.regexp_string "@") lab_str 2 in
+    let splitted = Strings.bounded_split '@' lab_str 2 in
     match splitted with
     | [before; after] -> before ^ to_append ^ "@" ^ after
     | _ -> lab_str^to_append in
@@ -72,11 +72,11 @@ let append_to_model_trace_label ~labels ~to_append =
 
 let get_model_element_name ~labels =
   let trace_label = get_model_trace_label ~labels in
-  let splitted1 = Str.bounded_split (Str.regexp_string ":") trace_label.lab_string 2 in
+  let splitted1 = Strings.bounded_split ':' trace_label.lab_string 2 in
   match splitted1 with
   | [_; content] ->
     begin
-      let splitted2 = Str.bounded_split (Str.regexp_string "@") content 2 in
+      let splitted2 = Strings.bounded_split '@' content 2 in
       match splitted2 with
       | [el_name; _] -> el_name
       | [el_name] -> el_name
@@ -87,7 +87,7 @@ let get_model_element_name ~labels =
 
 let get_model_trace_string ~labels =
   let tl = get_model_trace_label ~labels in
-  let splitted = Str.bounded_split (Str.regexp_string ":") tl.lab_string 2 in
+  let splitted = Strings.bounded_split ':' tl.lab_string 2 in
   match splitted with
   | [_; t_str] -> t_str
   | _ -> ""
diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml
index fcf3b4f5eda17788919e436676b72cce8669f243..2403fd9ef0d39a356b75f6c60161fd59c5208bfb 100644
--- a/src/core/model_parser.ml
+++ b/src/core/model_parser.ml
@@ -113,8 +113,8 @@ type model_element = {
 }
 
 let split_model_trace_name mt_name =
-  (** Mt_name is of the form "name[@type[@*]]". Return (name, type) *)
-  let splitted = Str.bounded_split (Str.regexp_string "@") mt_name 3 in
+  (* Mt_name is of the form "name[@type[@*]]". Return (name, type) *)
+  let splitted = Strings.bounded_split '@' mt_name 3 in
   match splitted with
   | [first] -> (first, "")
   | first::second::_ -> (first, second)
diff --git a/src/driver/autodetection.ml b/src/driver/autodetection.ml
index 4bfbdf6e32ee46602e65055076caedcb2e035275..df4abdf295505faa0a0f47f5cba3b986432b8efb 100644
--- a/src/driver/autodetection.ml
+++ b/src/driver/autodetection.ml
@@ -365,7 +365,7 @@ let detect_exec env main data acc exec_name =
     match data.prover_command with
     | None ->
       (* Empty prover *)
-      if good || old then begin (** Known version with error *)
+      if good || old then begin (* Known version with error *)
         known_version env exec_name;
         eprintf "Found prover %s version %s%s@."
           data.prover_name ver
diff --git a/src/driver/whyconf.ml b/src/driver/whyconf.ml
index 5c87abb0976486038a7b6eea949b18b9ba726751..d7309e4d11c17db7a5376215ff25b03cff3c5a58 100644
--- a/src/driver/whyconf.ml
+++ b/src/driver/whyconf.ml
@@ -673,7 +673,7 @@ let merge_config config filename =
       let plugins =
         (get_stringl ~default:[] rc "plugin") @ config.main.plugins in
       { config.main with loadpath = loadpath; plugins = plugins } in
-  (** get more strategies *)
+  (* get more strategies *)
   let more_strategies = get_strategies rc in
   let strategies =
     List.fold_left load_strategy config.strategies more_strategies
diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml
index 72a8b205ad3928568871d0b43b3d3df30aef906e..7ea27a315a590cf55c946c09d791250b83552544 100644
--- a/src/ide/gmain.ml
+++ b/src/ide/gmain.ml
@@ -810,7 +810,7 @@ let () = w#show ()
 (** TODO remove that should done only in session *)
 let project_dir =
   let fname = Queue.pop files in
-  (** The remaining files in [files] are going to be open *)
+  (* The remaining files in [files] are going to be open *)
   if Sys.file_exists fname then
     begin
       if Sys.is_directory fname then
diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml
index 994cb89a730ec6415f955740b1218264838ceda2..aa0e2d520942701ace312f92249d3ddd97aba836 100644
--- a/src/printer/smtv2.ml
+++ b/src/printer/smtv2.ml
@@ -229,7 +229,7 @@ let model_trace_for_postcondition ~labels info =
       labels
 
 let get_fun_name name =
-  let splitted = Str.bounded_split (Str.regexp_string ":") name 2 in
+  let splitted = Strings.bounded_split ':' name 2 in
   match splitted with
   | _::[second] ->
     second
diff --git a/src/session/termcode.ml b/src/session/termcode.ml
index 7e6b062afaedb529703fa837b4ad66c15c992bd4..4e7cf2651261ede6458e96f639c2f1788b2714d3 100644
--- a/src/session/termcode.ml
+++ b/src/session/termcode.ml
@@ -21,7 +21,7 @@ let collect_expls lab =
     (fun lab acc ->
        let lab = lab.Ident.lab_string in
        try
-         let s = Lexlib.remove_prefix "expl:" lab in s :: acc
+         let s = Strings.remove_prefix "expl:" lab in s :: acc
        with Not_found -> acc)
     lab
     []
diff --git a/src/transform/intro_projections_counterexmp.ml b/src/transform/intro_projections_counterexmp.ml
index 75fec3d0d9efdcffa4391d0de13b3f7f6d54845b..2aa2aa2a723f440d4d56aad9c585c3de8cc3f18b 100644
--- a/src/transform/intro_projections_counterexmp.ml
+++ b/src/transform/intro_projections_counterexmp.ml
@@ -50,7 +50,7 @@ let intro_const_equal_to_term
     ~const_name
     ~axiom_name
     =
-  (** See documentation of the function in file intro_projections_counterexmp.mli. *)
+  (* See documentation of the function in file intro_projections_counterexmp.mli. *)
 
   (* Create declaration of new constant *)
   (*let lab_new = Slab.add model_label labels in*)
diff --git a/src/transform/intro_vc_vars_counterexmp.ml b/src/transform/intro_vc_vars_counterexmp.ml
index 8f859f8c74d4bb8329e93d4885c7eb5f0c3712ed..4063bff16d2269b7528f0d8cb8c0c6d0dfb240cb 100644
--- a/src/transform/intro_vc_vars_counterexmp.ml
+++ b/src/transform/intro_vc_vars_counterexmp.ml
@@ -198,7 +198,7 @@ let get_location_of_vc task =
   let meta_args = Task.on_meta_excl meta_vc_location task in
   match meta_args with
   | Some [Theory.MAstr loc_str] ->
-    let splitted = Str.bounded_split (Str.regexp_string ":") loc_str 4 in
+    let splitted = Strings.bounded_split ':' loc_str 4 in
     let loc =  match splitted with
       | [filename; line; col1; col2] ->
 	let line = int_of_string line in
diff --git a/src/util/lexlib.mli b/src/util/lexlib.mli
index fac531d6d32a549dc5ca9f6c1918629cc4834865..ef72eb57f4f3b8aa61fd3d9058912aecd2f68181 100644
--- a/src/util/lexlib.mli
+++ b/src/util/lexlib.mli
@@ -22,10 +22,3 @@ val update_loc : Lexing.lexbuf -> string option -> int -> int -> unit
 val remove_leading_plus : string -> string
 
 val remove_underscores : string -> string
-
-val has_prefix : string -> string -> bool
-(** [has_prefix pref s] returns true if s [s] starts with prefix [pref] *)
-
-val remove_prefix : string -> string -> string
-(** [remove_prefix pref s] removes the prefix [pref] from [s]. Raises
-    [Not_found if [s] does not start with [pref] *)
diff --git a/src/util/lexlib.mll b/src/util/lexlib.mll
index ab82a197674fde738098069eff27a11c4d358d4d..1e16e78281730608725fa74cc8e3298cc7702f4d 100644
--- a/src/util/lexlib.mll
+++ b/src/util/lexlib.mll
@@ -104,18 +104,4 @@ and string = parse
       t
     end else s
 
-let has_prefix pref s =
-  let l = String.length pref in
-  if String.length s < l then false else
-    try
-      for i = 0 to l - 1 do if s.[i] <> pref.[i] then raise Exit done;
-      true
-    with Exit -> false
-
-let remove_prefix pref s =
-  let l = String.length pref in
-  if String.length s < l then raise Not_found else
-  for i = 0 to l - 1 do if s.[i] <> pref.[i] then raise Not_found done;
-  String.sub s l (String.length s - l)
-
 }
diff --git a/src/util/strings.ml b/src/util/strings.ml
index 6b0c0f75b6a7df193366c99e84e83f09568413a9..ca59a937601dd7efc982eba02a01f2221fe2f455 100644
--- a/src/util/strings.ml
+++ b/src/util/strings.ml
@@ -15,7 +15,6 @@ let copy = String.copy
 let set = String.set
 
 
-
 let rev_split c s =
   let rec aux acc i =
     try
@@ -27,6 +26,18 @@ let rev_split c s =
 
 let split c s = List.rev (rev_split c s)
 
+let rev_bounded_split c s n =
+  let rec aux acc i n =
+    if n = 1 then acc else
+    try
+      let j = String.index_from s i c in
+      aux ((String.sub s i (j-i))::acc) (j+1) (n-1)
+    with Not_found -> (String.sub s i (String.length s - i))::acc
+      | Invalid_argument _ -> ""::acc in
+  aux [] 0 n
+
+let bounded_split c s n = List.rev (rev_bounded_split c s n)
+
 let ends_with s suf =
   let rec aux s suf suflen offset i =
     i >= suflen || (s.[i + offset] = suf.[i]
@@ -45,3 +56,17 @@ let pad_right c s i =
   else if sl > i
   then String.sub s 0 i
   else s
+
+let has_prefix pref s =
+  let l = String.length pref in
+  if String.length s < l then false else
+    try
+      for i = 0 to l - 1 do if s.[i] <> pref.[i] then raise Exit done;
+      true
+    with Exit -> false
+
+let remove_prefix pref s =
+  let l = String.length pref in
+  if String.length s < l then raise Not_found else
+  for i = 0 to l - 1 do if s.[i] <> pref.[i] then raise Not_found done;
+  String.sub s l (String.length s - l)
diff --git a/src/util/strings.mli b/src/util/strings.mli
index 3d5c2c0c92ec697b90f51e5c203a34ad5e6a612b..b28c026e892847fb575f013e0a592287d19ea5a7 100644
--- a/src/util/strings.mli
+++ b/src/util/strings.mli
@@ -22,9 +22,24 @@ val set : string -> int -> char -> unit
 val rev_split : char -> string -> string list
 
 val split : char -> string -> string list
+(** [split c s] splits [s] into substrings, taking as delimiter the
+    character [c], and returns the list of substrings.  An occurrence of
+    the delimiter at the beginning or at the end of the string is
+    ignored. *)
+
+val bounded_split : char -> string -> int -> string list
+(** [bounded_split c s n] do the same as [split c s] but splits into
+    [n] substring at most *)
 
 val ends_with : string -> string -> bool
 (** test if a string ends with another *)
 
 val pad_right : char -> string -> int -> string
 (** chop or pad the given string on the right up to the given length *)
+
+val has_prefix : string -> string -> bool
+(** [has_prefix pref s] returns true if s [s] starts with prefix [pref] *)
+
+val remove_prefix : string -> string -> string
+(** [remove_prefix pref s] removes the prefix [pref] from [s]. Raises
+    [Not_found if [s] does not start with [pref] *)
diff --git a/src/why3session/why3session_csv.ml b/src/why3session/why3session_csv.ml
index 26bd2390743f59b7f6fb16bdd74ed77df94f4533..eab8c6535fba7cba9343300d2485412e9da6503d 100644
--- a/src/why3session/why3session_csv.ml
+++ b/src/why3session/why3session_csv.ml
@@ -111,7 +111,7 @@ let rec print_line fmt provers a =
         fprintf fmt ",%a" print_cell pa
       with Not_found ->
         fprintf fmt ",") provers;
-    fprintf fmt "\n@?" (** no @\n since we use Pp.wnl *)
+    fprintf fmt "\n@?" (* no @\n since we use Pp.wnl *)
   | _ -> () end;
   Session.iter (print_line fmt provers) a
 
@@ -195,20 +195,20 @@ let print_provers_time (provers_time : float list Whyconf.Hprover.t) fmt =
     let sorted = List.fast_sort Pervasives.compare l in
     (ref sorted,ref 0)) l in
   let rec print_line (l : (float list ref * int ref) list) =
-    (** get the minimum *)
+    (* get the minimum *)
     let lmin = List.fold_left (fun acc (e,_) ->
       match !e with
       | [] -> acc
       | a::_ -> min a acc) max_float l in
-    if lmin = max_float then () (** finished *)
+    if lmin = max_float then () (* finished *)
     else begin
-      (** remove the minimum and increase the number of proved *)
+      (* remove the minimum and increase the number of proved *)
       let rec remove nb = function
         | [] -> []
         | a::e when a = lmin -> incr nb; remove nb e
         | e -> e in
       List.iter (fun (e,nb) -> e:=remove nb !e) l;
-      (** Print the current number of proved *)
+      (* Print the current number of proved *)
       fprintf fmt "%f,%a\n@?" lmin
         (Pp.print_list Pp.comma (fun fmt (_,nb) -> pp_print_int fmt (!nb)))
         l;
@@ -251,7 +251,7 @@ let print_file out f : unit =
 
 let print_args fmt args =
   (Pp.print_iter1 Array.iter
-     (fun fmt () -> Format.pp_print_string fmt " ") (** no @\n *)
+     (fun fmt () -> Format.pp_print_string fmt " ") (* no @\n *)
      (fun fmt -> Format.fprintf fmt "%S"))
    fmt args
 
@@ -271,10 +271,10 @@ let call_gnuplot arg1 arg2 csv_file gp_file =
 let run_by_time_gen dir canonical_name iter =
   let to_remove = Stack.create () in
   let canonical_name = Filename.concat dir canonical_name in
-  (** compute stats *)
+  (* compute stats *)
   let provers_time = Whyconf.Hprover.create 5 in
   iter provers_time;
-  (** print .csv if necessary *)
+  (* print .csv if necessary *)
   let csv_file =
      if !opt_gnuplot = [] || !opt_print_csv then
        let fname = canonical_name ^ ".csv" in
@@ -290,7 +290,7 @@ let run_by_time_gen dir canonical_name iter =
      else None
   in
 
-  (** create .gp if necessary *)
+  (* create .gp if necessary *)
   let nb_provers = Whyconf.Hprover.length provers_time in
   let gp_file =
     if List.mem GP !opt_gnuplot
@@ -307,7 +307,7 @@ let run_by_time_gen dir canonical_name iter =
     else None
   in
 
-  (** output .png, .pdf, .csv and run .qt if necessary *)
+  (* output .png, .pdf, .csv and run .qt if necessary *)
   if List.mem PNG !opt_gnuplot then
     call_gnuplot
       "set terminal pngcairo size 600, 400"
@@ -328,7 +328,7 @@ let run_by_time_gen dir canonical_name iter =
       "set terminal qt persist"
       ""
       csv_file gp_file;
-  (** Clean up temporary files *)
+  (* Clean up temporary files *)
   Stack.iter Sys.remove to_remove
 
 
diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml
index 65224dc80586a21d7f96e824d518cd7e4d3bc466..cf60dee324bc67256c3d399429d25d3210db7255 100644
--- a/src/why3session/why3session_html.ml
+++ b/src/why3session/why3session_html.ml
@@ -382,7 +382,7 @@ struct
       base_dst
     with Not_found ->
       eprintf "Default %s@." basename;
-      (** default printer *)
+      (* default printer *)
       let base = try Filename.chop_extension basename with _ -> basename in
       let base_dst = base^".txt" in
       if !opt_context then
@@ -529,7 +529,7 @@ $(function () {\
     iter_files (run_file context print_session);
     if !opt_context then
       let data_dir = Whyconf.datadir (Whyconf.get_main config) in
-      (** copy images *)
+      (* copy images *)
       let img_dir_src = Filename.concat data_dir "images" in
       let img_dir_src = Filename.concat img_dir_src "boomy" in
       let img_dir_dst = Filename.concat !output_dir "images" in
@@ -539,7 +539,7 @@ $(function () {\
         let to_  = Filename.concat img_dir_dst img_name in
         Sysutil.copy_file from to_)
         ["folder16.png";"file16.png";"wizard16.png";"configure16.png"];
-      (** copy javascript *)
+      (* copy javascript *)
       let js_dir_src = Filename.concat data_dir "javascript" in
       let js_dir_dst = Filename.concat !output_dir "javascript" in
       Sysutil.copy_dir js_dir_src js_dir_dst
diff --git a/src/why3session/why3session_latex.ml b/src/why3session/why3session_latex.ml
index 589ddb18ab695097fbf4d23fd40527d481e8122f..85729961779dfaef585d28a821aa31e0b2815cd9 100644
--- a/src/why3session/why3session_latex.ml
+++ b/src/why3session/why3session_latex.ml
@@ -302,16 +302,16 @@ let latex_longtable n fmt depth name provers t=
   (* First head *)
   print_head n depth provers fmt;
   fprintf fmt "\\hline \\endfirsthead @.";
-  (** Other heads : "Continued... " added *)
+  (* Other heads : "Continued... " added *)
   fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
 \\\\ @." (List.length provers + 1) ;
   fprintf fmt "\\hline @.";
   print_head n depth provers fmt;
   fprintf fmt "\\hline \\endhead @.";
-  (** Other foots : "Continued..." added *)
+  (* Other foots : "Continued..." added *)
   fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
 \\\\ @." (List.length provers);
-  (** Last foot : nothing *)
+  (* Last foot : nothing *)
   fprintf fmt "\\endfoot \\endlastfoot @.";
   if n == 1 then
     List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
diff --git a/src/why3session/why3session_output.ml b/src/why3session/why3session_output.ml
index 38373c2b2db0494b3611a58a7382685d6d61a4d6..edbd5591d369813e75afadb876dcf554a7497a6e 100644
--- a/src/why3session/why3session_output.ml
+++ b/src/why3session/why3session_output.ml
@@ -66,14 +66,14 @@ let run_one env config filters dir fname =
             Opt.get (goal_task_option pr.proof_parent) in
           match load_prover env_session pr.proof_prover with
           | None ->
-            (** In fact That is a bad reason we can always output know? *)
+            (* In fact That is a bad reason we can always output know? *)
             eprintf "Can't@ output@ task@ for@ prover@ %a@ not@ installed@."
               Whyconf.print_prover pr.proof_prover
           | Some lp ->
             let dest = Driver.file_of_task lp.prover_driver fname tname task in
-            (** Uniquify the filename before the extension if it exists*)
+            (* Uniquify the filename before the extension if it exists*)
             let i = try String.rindex dest '.' with _ -> String.length dest in
-            (** Before extension *)
+            (* Before extension *)
             let name = (String.sub dest 0 i) in
             let name = Ident.string_unique fname_printer name in
             let ext = String.sub dest i (String.length dest - i) in
@@ -89,7 +89,7 @@ let run () =
   let env,config,should_exit1 = read_env_spec () in
   let filters,should_exit2 = read_filter_spec config in
   if should_exit1 || should_exit2 then exit 1;
-  (** sanitize --to-prover and --to-known-prover for Copy* *)
+  (* sanitize --to-prover and --to-known-prover for Copy* *)
   match !opt_output_dir with
   | None ->
     eprintf "The@ option@ --output-dir/-o@ must@ be@ set@.";
diff --git a/src/why3session/why3session_run.ml b/src/why3session/why3session_run.ml
index d3026b97354fbd816e6e85f80dcb30317d713338..3dc338a93f136c85a7877de37acc10a79d0b83ce 100644
--- a/src/why3session/why3session_run.ml
+++ b/src/why3session/why3session_run.ml
@@ -181,7 +181,7 @@ let is_valid pr =
 
 let to_edit_queue = Queue.create ()
 
-let is_successful env = (** means all goals proved*)
+let is_successful env = (* means all goals proved*)
   try
     let rec iter = function
         | File f -> file_iter iter f
@@ -310,7 +310,7 @@ let run_one sched env config filters interactive_provers fname =
 	      callback in
           M.edit_proof_v3 env_session sched
 	    ~cntexample:false
-            ~default_editor:"" (** TODO? *)
+            ~default_editor:"" (* TODO? *)
             ~callback:callback_edit a
         else
           Todo.stop todo;
diff --git a/src/whyml/mlw_wp.ml b/src/whyml/mlw_wp.ml
index c0d7629cb28d6882e23cc6fd9bd4165f55940e00..922de7e6ed7658fd35a7339f049924718a921047 100644
--- a/src/whyml/mlw_wp.ml
+++ b/src/whyml/mlw_wp.ml
@@ -138,14 +138,8 @@ let expl_loopvar   = Ident.create_label "expl:loop variant decrease"
 let expl_variant   = Ident.create_label "expl:variant decrease"
 
 let lab_has_expl =
-(*
-  let expl_regexp = Str.regexp "expl:\\(.*\\)" in
-*)
   Slab.exists
-    (fun l -> Lexlib.has_prefix "expl:" l.lab_string)
-(*
-       Str.string_match expl_regexp l.lab_string 0)
-*)
+    (fun l -> Strings.has_prefix "expl:" l.lab_string)
 
 let rec wp_expl l f =
   if lab_has_expl f.t_label then f