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/safe_typing.ml | |
| 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/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bdffa68022..b8fe1571c8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -255,19 +255,19 @@ type global_declaration = let hcons_const_type = function | NonPolymorphicType t -> - NonPolymorphicType (hcons1_constr t) + NonPolymorphicType (hcons_constr t) | PolymorphicArity (ctx,s) -> - PolymorphicArity (map_rel_context hcons1_constr ctx,s) + PolymorphicArity (map_rel_context hcons_constr ctx,s) let hcons_const_body = function | Undef inl -> Undef inl | Def l_constr -> let constr = Declarations.force l_constr in - Def (Declarations.from_val (hcons1_constr constr)) + Def (Declarations.from_val (hcons_constr constr)) | OpaqueDef lc -> if lazy_constr_is_val lc then let constr = Declarations.force_opaque lc in - OpaqueDef (Declarations.opaque_from_val (hcons1_constr constr)) + OpaqueDef (Declarations.opaque_from_val (hcons_constr constr)) else OpaqueDef lc let hcons_constant_body cb = |