diff options
Diffstat (limited to 'engine/nameops.ml')
| -rw-r--r-- | engine/nameops.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/nameops.ml b/engine/nameops.ml index 15e201347c..2047772cfe 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -132,6 +132,7 @@ sig val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a val get_id : t -> Id.t val pick : t -> t -> t + val pick_annot : t Context.binder_annot -> t Context.binder_annot -> t Context.binder_annot val cons : t -> Id.t list -> Id.t list val to_option : Name.t -> Id.t option @@ -176,6 +177,11 @@ struct | Name _ -> na1 | Anonymous -> na2 + let pick_annot na1 na2 = + let open Context in + match na1.binder_name with + | Name _ -> na1 | Anonymous -> na2 + let cons na l = match na with | Anonymous -> l |