diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-02 19:54:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-02 19:54:48 +0000 |
| commit | d566330747374ba13d6b52424d53ab7d84cc921e (patch) | |
| tree | 9e084b143f44f531e2550343deaff67529ac8391 /kernel/type_errors.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/type_errors.mli')
0 files changed, 0 insertions, 0 deletions