Merge branch 'master' into stable; prepare for 0.4

Author: c-cube

src/core/Sexp_lex.mll

@@ -8,7 +8,9 @@
   exception Error of Location.t * string
 
   let remove_quotes s =
-    assert (s.[0] = '\'' && s.[String.length s - 1] = '\'');
+    assert (
+      (s.[0] = '\'' && s.[String.length s - 1] = '\'') ||
+      (s.[0] = '"' && s.[String.length s - 1] = '"'));
     String.sub s 1 (String.length s - 2)
 }
 

src/core/Utils.ml

@@ -231,7 +231,7 @@ let singleton_if check ~f x = if check then [f x] else []
 
 let arg_choice l f =
   let pick s =
-    let s = s |> String.trim |> String.lowercase_ascii in
+    let s = s |> String.trim |> CCString.lowercase_ascii in
     try f (List.assoc s l)
     with Not_found -> assert false
   in
@@ -303,7 +303,7 @@ let () =
 
 exception NotImplemented of string
 
-let pp_with_sep sep out () = Format.fprintf out "%s@ " sep
+let pp_with_sep sep out () = Format.fprintf out "%s@," sep
 let pp_seq ?(sep=" ") p = CCFormat.seq ~sep:(pp_with_sep sep) p
 let pp_list ?(sep=" ") p = CCFormat.list ~sep:(pp_with_sep sep) p
 

src/main/nunchaku.ml

@@ -101,7 +101,7 @@ let output_opt = Utils.arg_choice outputs_ ((:=) output_)
 
 (* solver string specification *)
 let parse_solvers_ s =
-  let s = String.trim s |> String.lowercase_ascii in
+  let s = String.trim s |> CCString.lowercase_ascii in
   let l = CCString.Split.list_cpy ~by:"," s in
   List.map
     (function

src/parsers/TPTP_print.ml

@@ -219,7 +219,7 @@ and mk_var ~state v =
   let name = ID.name (Var.id v) in
   let name = match name.[0] with
     | 'A' .. 'Z' -> name
-    | 'a' .. 'b' -> String.capitalize_ascii name
+    | 'a' .. 'b' -> CCString.capitalize_ascii name
     | _ -> "V" ^ name
   in
   Var.make ~name ~ty:(preprocess_ty ~state (Var.ty v))