From 33c93006b7685092b5239ea001058578fac3552f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 16 Oct 2018 01:28:36 +0200 Subject: [clib] Deprecate string functions available in OCaml 4.05 - `CString.strip -> String.trim` - `CString.split -> String.split_on_char` As noted by @ppedrot there are some small differences on semantics: > OCaml's `trim` also takes line feeds (LF) into account. Similarly, > OCaml's `split` never returns an empty list whereas Coq's `split` > does on the empty string. --- plugins/ltac/profile_ltac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index d22bd4967a..db7dcfa6ef 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -260,7 +260,7 @@ let string_of_call ck = ) in let s = String.map (fun c -> if c = '\n' then ' ' else c) s in let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in - CString.strip s + String.trim s let rec merge_sub_tree name tree acc = try -- cgit v1.2.3