aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-11-21 09:23:47 +0100
committerPierre-Marie Pédrot2019-11-22 08:35:57 +0100
commitb8b835cbb7ce5fa12a60184fd83fbde2082d51b3 (patch)
tree195f3539dbd72866624506c800dec1d6da611bfd /dev
parent83ab871c90c862ebb08bcc549701beec0afc6cce (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 'dev')
0 files changed, 0 insertions, 0 deletions