diff options
Diffstat (limited to 'library/nameops.ml')
| -rw-r--r-- | library/nameops.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index e4c75bd760..b68c095936 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -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 |