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/cClosure.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index bd04677374..2852d48a5d 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -114,9 +114,9 @@ type fterm =
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
-  | FProd of Name.t * fconstr * constr * fconstr subs
-  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
+  | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
+  | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
   | FLIFT of int * fconstr
@@ -165,7 +165,7 @@ val mk_red : fterm -> fconstr
 val fterm_of : fconstr -> fterm
 val term_of_fconstr : fconstr -> constr
 val destFLambda :
-  (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
+  (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t Context.binder_annot * fconstr * fconstr
 
 (** Global and local constant cache *)
 type clos_infos
-- 
cgit v1.2.3


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