diff options
| author | notin | 2006-04-28 14:25:31 +0000 |
|---|---|---|
| committer | notin | 2006-04-28 14:25:31 +0000 |
| commit | 78fff376f71ce6538dad42be95b074a916a4ce49 (patch) | |
| tree | e90f7771e62c0c37230ce1de383fddcc6ba50e8f /lib/util.ml | |
| parent | f255f2af3ab46d200bb22fbe68500b57f8c02721 (diff) | |
r8931@thot: notin | 2006-04-28 16:19:38 +0200
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml index 04086e20f3..a9d9655eda 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -363,7 +363,19 @@ let list_prefix_of prefl l = | ([], _) -> true | (_, _) -> false in - prefrec (prefl,l) + prefrec (prefl,l) + +let list_drop_prefix p l = +(* if l=p++t then return t else l *) + let rec list_drop_prefix_rec = function + | ([], tl) -> Some tl + | (_, []) -> None + | (h1::tp, h2::tl) -> + if h1 = h2 then list_drop_prefix_rec (tp,tl) else None + in + match list_drop_prefix_rec (p,l) with + | Some r -> r + | None -> l let list_map_append f l = List.flatten (List.map f l) |