diff options
| author | Gaëtan Gilbert | 2019-11-24 22:41:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-24 22:41:11 +0100 |
| commit | 7177a6f76e74eb6e97c634bad484027bf94979bd (patch) | |
| tree | c8e3cb7d4496f27714e08015e81e955dce29e1d4 /kernel/retypeops.mli | |
| parent | 27e4f306d54f2cc04b40d740584a7b3eda2d490a (diff) | |
| parent | b8b835cbb7ce5fa12a60184fd83fbde2082d51b3 (diff) | |
Merge PR #11152: Cache the relevance flag in rel contexts in an efficient way.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/retypeops.mli')
| -rw-r--r-- | kernel/retypeops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli index f4497be44b..dd4513959f 100644 --- a/kernel/retypeops.mli +++ b/kernel/retypeops.mli @@ -14,14 +14,14 @@ val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance -val relevance_of_fterm : Environ.env -> Sorts.relevance list -> +val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t -> Esubst.lift -> CClosure.fconstr -> Sorts.relevance (** Helpers *) open Names -val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance +val relevance_of_rel : Environ.env -> int -> Sorts.relevance val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance |