From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 engine/nameops.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/nameops.ml')

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
-- 
cgit v1.2.3