diff options
| author | Gaëtan Gilbert | 2018-10-02 14:29:52 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | f3c1fe8bc7979cd7036fcd2a1b2fe8f0a1acb058 (patch) | |
| tree | caa76fac83aeca1e2be5289b03287cb3319d8869 /kernel/cClosure.mli | |
| parent | 0b2e68030ec188a4865021bcf2c16f2242289c4b (diff) | |
mutable relevance marks in fconstr
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 5 |
1 files changed, 5 insertions, 0 deletions
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 |