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.
---
 kernel/declareops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 23a44433b3..54a853fc81 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -70,6 +70,8 @@ val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj
 val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
   Names.Projection.Repr.t array option
 
+val relevance_of_projection_repr : mutual_inductive_body -> Names.Projection.Repr.t -> Sorts.relevance
+
 (** {6 Kernel flags} *)
 
 (** A default, safe set of flags for kernel type-checking *)
-- 
cgit v1.2.3