diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-09 09:50:19 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-09 09:50:19 +0000 |
| commit | 0016ab21e8f9564350a6319126f47313a338c115 (patch) | |
| tree | 82373c1cb18487fb0b6dffdc65c107157587c97c | |
| parent | 9fc97fa94f3d2912fc6e5bbb3c0022a96b0c1c6c (diff) | |
implode codé avec String.concat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@68 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/util.ml | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/lib/util.ml b/lib/util.ml index 34ad89aa2..a26cb60d8 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -24,17 +24,7 @@ let explode s = in explode_rec 0 -let implode sl = - let len = List.fold_left (fun a b -> a + (String.length b)) 0 sl in - let dest = String.create len in - let _ = List.fold_left - (fun start src -> - let src_len = String.length src in - String.blit src 0 dest start src_len; - start + src_len) - 0 sl - in - dest +let implode sl = String.concat "" sl let parse_section_path s = let len = String.length s in |