diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /library/nameops.ml | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'library/nameops.ml')
| -rw-r--r-- | library/nameops.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index 1c6a7d56..779f3389 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 8727 2006-04-24 09:48:06Z herbelin $ *) +(* $Id: nameops.ml 9225 2006-10-09 15:59:23Z herbelin $ *) open Pp open Util @@ -154,6 +154,10 @@ let name_app f = function | Name id -> Name (f id) | Anonymous -> Anonymous +let name_fold_map f e = function + | Name id -> let (e,id) = f e id in (e,Name id) + | Anonymous -> e,Anonymous + let next_name_away_with_default default name l = match name with | Name str -> next_ident_away str l |