diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-20 08:22:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-20 08:22:51 +0000 |
commit | ec2948e7848265dbf547d97f0866ebd8f5cb6c97 (patch) | |
tree | 15c8ca8918a8a633c7664d564b14efb8f987385a /library/global.mli | |
parent | 5275368649a254835a5277dfa185506713506618 (diff) |
Declareops + Modops : more clever substitutions
We try harder to preserve pointer equality when substituting.
This will probably have little effect (for instance the
constr_substituted are anyway _never_ substituted in place),
but it cannot harm.
Two particular cases:
- we try to share (and maintain shared) mind_user_lc and mind_nf_lc
- we try to share (and maintain shared) mod_expr and mod_type
TODO: check that native compiler is still ok, since we might have
less (ref NotLinked) now. Having references in constant_body and co
is anyway a Very Bad Idea (TM).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions