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

0 files changed, 0 insertions, 0 deletions