From f3c1fe8bc7979cd7036fcd2a1b2fe8f0a1acb058 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Oct 2018 14:29:52 +0200
Subject: mutable relevance marks in fconstr

---
 kernel/cClosure.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 2852d48a5d..b1b69dded8 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -167,6 +167,11 @@ val term_of_fconstr : fconstr -> constr
 val destFLambda :
   (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t Context.binder_annot * fconstr * fconstr
 
+type optrel = Unknown | KnownR | KnownI
+
+val relevance_of : fconstr -> optrel
+val set_relevance : Sorts.relevance -> fconstr -> unit
+
 (** Global and local constant cache *)
 type clos_infos
 type clos_tab
-- 
cgit v1.2.3