diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-26 13:17:53 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-26 13:17:53 +0000 |
commit | f757348648841b0ed3d1f6eb96046bbf8c43ea4e (patch) | |
tree | af90b542e953279528d96d1d69d18e664b668975 /kernel/mod_subst.ml | |
parent | 68801aa95021bfc4da2de028b1366fcbdf42bcde (diff) |
Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo
It appears that registration of hints is the only place (at least
when compiling stdlib) where Univ.universes (the graph of universes)
is stored in vo. More precisely, a Hint Resolve will place in vo
a pri_auto_tactic, which may contain some clausenv, which contain
both a env and a evar_map, each of them containing a Univ.universes
In fact, even env and evar_map are also never stored in vo apart
from hints registration.
Currently, there's nothing wrong in this storing of env / evar_map /
universes. In fact, it seems that every stored universes are actually
empty. Same for env, thanks to awkward lines { cl with env=empty_env }.
But this may hinder potential evolutions of Univ.universes toward a
private per-session representation. Conclusion: it is cleaner
(and not that hard) to store a Term.types instead of the clausenv
in vo, and reconstitute the clausenv at Require-time. On a compilation
of the stdlib, the time effect is hardly noticable (<1%).
NB: a Univ.universes is also stored in initial.coq, but this is a
different story (Write State ...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14611 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.ml')
0 files changed, 0 insertions, 0 deletions