Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

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