diff options
| author | letouzey | 2011-10-02 19:54:48 +0000 |
|---|---|---|
| committer | letouzey | 2011-10-02 19:54:48 +0000 |
| commit | d566330747374ba13d6b52424d53ab7d84cc921e (patch) | |
| tree | 9e084b143f44f531e2550343deaff67529ac8391 /kernel/term.mli | |
| parent | 85a870d3e8f3f26222245af4d0d2a54ccf52eeb8 (diff) | |
Hash-consing of constr could share more
- An inductive is hidden inside case_info.
(btw, maybe we could get rid of this ci_ind altogether,
since the information is already in the predicate of the match)
- Typical situation where user kn and canonical kn are initially (==)
was not preserved by hconsing of constant / mutual_inductive
- inductive = (mutual_inductive * int) and
constructor = inductive * int were not properly shared
This should fix the strange situation of Udine/PiCalc taking *more*
vo space after the last round of hcons tweaks.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14507 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 2ec1bd9b96..c556d0a077 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -626,8 +626,8 @@ val hash_constr : constr -> int (*********************************************************************) -val hcons1_constr : constr -> constr -val hcons1_types : types -> types +val hcons_constr : constr -> constr +val hcons_types : types -> types (**************************************) |