diff options
| author | letouzey | 2011-10-10 22:54:21 +0000 |
|---|---|---|
| committer | letouzey | 2011-10-10 22:54:21 +0000 |
| commit | 2484db1991dac3b41d70130cf4c8697cb8c4af9a (patch) | |
| tree | 043c3b4e20498ff5257fd70bafb734614ed02169 /kernel/declarations.mli | |
| parent | 73383084bf8bb273775707ffc1f4f18eb5752db3 (diff) | |
Hash-consing of mutual_inductive_body (and Univ.constraints)
Inductive definitions aren't that big, but they may contain some
constr (in types, rel_context, etc), hence if we hash-cons the
constr in Definition but not these ones, we may loose some sharing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14544 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ebedd17e67..5b800edeca 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -62,8 +62,6 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr -val subst_constant_def : substitution -> constant_def -> constant_def - type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -71,6 +69,7 @@ type constant_body = { const_body_code : to_patch_substituted; const_constraints : constraints } +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 or const_body_opaque ? *) @@ -233,3 +232,13 @@ and module_type_body = typ_constraints : constraints; (** quotiented set of equivalent constant and inductive name *) typ_delta :delta_resolver} + + +(** Hash-consing *) + +(** Here, strictly speaking, we don't perform true hash-consing + of the structure, but simply hash-cons all inner constr + and other known elements *) + +val hcons_const_body : constant_body -> constant_body +val hcons_mind : mutual_inductive_body -> mutual_inductive_body |