diff options
| author | Pierre-Marie Pédrot | 2019-11-21 09:23:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-22 08:35:57 +0100 |
| commit | b8b835cbb7ce5fa12a60184fd83fbde2082d51b3 (patch) | |
| tree | 195f3539dbd72866624506c800dec1d6da611bfd /kernel/retypeops.mli | |
| parent | 83ab871c90c862ebb08bcc549701beec0afc6cce (diff) | |
Use the relevance flag in CClosure rel contexts in an efficient way.
Rels that exist inside the environment at the time of the closure creation
are fetched in the global environment, while we only use the local list of
relevance for FRels. All the infrastructure was implicitly relying on this
kind of behaviour before the introduction of SProp.
Fixes #11150: pattern is 10x slower in Coq 8.10.0
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 |