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 /kernel/declareops.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 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0da7c85c7..54eed5ea6 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -14,7 +14,6 @@ open Mod_subst (** {6 Constants} *) -val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body (** Is there a actual body in const_body ? *) |