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/term_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/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 7551c31d4..cc9366c11 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -94,8 +94,8 @@ let infer_declaration env dcl = | DefinitionEntry c -> let (j,cst) = infer env c.const_entry_body in let j = - {uj_val = hcons1_constr j.uj_val; - uj_type = hcons1_constr j.uj_type} in + {uj_val = hcons_constr j.uj_val; + uj_type = hcons_constr j.uj_type} in let (typ,cst) = constrain_type env j cst c.const_entry_type in let def = if c.const_entry_opaque @@ -105,7 +105,7 @@ let infer_declaration env dcl = def, typ, cst | ParameterEntry (t,nl) -> let (j,cst) = infer env t in - let t = hcons1_constr (Typeops.assumption_of_judgment env j) in + let t = hcons_constr (Typeops.assumption_of_judgment env j) in Undef nl, NonPolymorphicType t, cst let global_vars_set_constant_type env = function |