Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

1 files changed, 19 insertions, 0 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 1e4e4e00b4..09c98ca1bc 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -128,6 +128,25 @@ module Hsorts =
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
 
+(** On binders: is this variable proof relevant *)
+type relevance = Relevant | Irrelevant
+
+let relevance_equal r1 r2 = match r1,r2 with
+  | Relevant, Relevant | Irrelevant, Irrelevant -> true
+  | (Relevant | Irrelevant), _ -> false
+
+let relevance_of_sort_family = function
+  | InSProp -> Irrelevant
+  | _ -> Relevant
+
+let relevance_hash = function
+  | Relevant -> 0
+  | Irrelevant -> 1
+
+let relevance_of_sort = function
+  | SProp -> Irrelevant
+  | _ -> Relevant
+
 let debug_print = function
   | SProp -> Pp.(str "SProp")
   | Prop -> Pp.(str "Prop")