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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f089b242a2..d2af957b54 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -264,16 +264,19 @@ let relevance_of_term env sigma c = if Environ.sprop_allowed env then let rec aux rels c = match kind sigma c with - | Rel n -> Retypeops.relevance_of_rel_extra env rels n + | Rel n -> + let len = Range.length rels in + if n <= len then Range.get rels (n - 1) + else Retypeops.relevance_of_rel env (n - len) | Var x -> Retypeops.relevance_of_var env x | Sort _ -> Sorts.Relevant | Cast (c, _, _) -> aux rels c | Prod ({binder_relevance=r}, _, codom) -> - aux (r::rels) codom + aux (Range.cons r rels) codom | Lambda ({binder_relevance=r}, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | LetIn ({binder_relevance=r}, _, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | App (c, _) -> aux rels c | Const (c,_) -> Retypeops.relevance_of_constant env c | Ind _ -> Sorts.Relevant @@ -287,7 +290,7 @@ let relevance_of_term env sigma c = | Meta _ | Evar _ -> Sorts.Relevant in - aux [] c + aux Range.empty c else Sorts.Relevant let relevance_of_type env sigma t = |