diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-24 16:22:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-24 16:22:00 +0000 |
| commit | 03406a6bc9ce34337d8631f7be26d152de984356 (patch) | |
| tree | 62d62baf78fb3db470ede00ac10f333b9403ef9a | |
| parent | 7ddef6f71e017af324113ae43c0fe2a5abc09764 (diff) | |
Completing r14448 and thus continuing r14407 (using Cast to propagate
information coming from tactics on how to solve cst/cst critical pairs
in the kernel conversion machine).
In r14448, extra Cast's were removed from kernel type-checker but
(erroneously) not from the terms actually registered in the
environment.
The current commit completes the work by registering the term output
by the type-checker and not the original term. Note that this needs to
move hconsing from before to after typing.
On the Coq library, propagating Cast (without keeping them on disk)
induces a stable 1% speedup (Xeon w3540). Having hcons before or after
type-checking makes no difference. It remains to test on user contribs
whether the current commit compensates the slow down and vo size
increasing coming with the improvement made to Qed in r14407.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14492 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | kernel/term_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | library/declare.ml | 9 |
3 files changed, 6 insertions, 11 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2c784e00e..7551c31d4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -93,6 +93,9 @@ let infer_declaration env dcl = match dcl with | 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 let (typ,cst) = constrain_type env j cst c.const_entry_type in let def = if c.const_entry_opaque @@ -102,7 +105,8 @@ let infer_declaration env dcl = def, typ, cst | ParameterEntry (t,nl) -> let (j,cst) = infer env t in - Undef nl, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst + let t = hcons1_constr (Typeops.assumption_of_judgment env j) in + Undef nl, NonPolymorphicType t, cst let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 6e0e098c0..49106c912 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -483,7 +483,7 @@ let infer env constr = let (j,(cst,_)) = execute env constr (empty_constraint, universes env) in assert (eq_constr j.uj_val constr); - ({ j with uj_val = constr }, cst) + (j, cst) let infer_type env constr = let (j,(cst,_)) = diff --git a/library/declare.ml b/library/declare.ml index df87153de..3a640c971 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -154,14 +154,6 @@ let inConstant = subst_function = ident_subst_function; discharge_function = discharge_constant } -let hcons_constant_declaration = function - | DefinitionEntry ce when !Flags.hash_cons_proofs -> - DefinitionEntry - { const_entry_body = hcons1_constr ce.const_entry_body; - const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque } - | cd -> cd - let declare_constant_common id dhyps (cd,kind) = let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in let c = Global.constant_of_delta (constant_of_kn kn) in @@ -171,7 +163,6 @@ let declare_constant_common id dhyps (cd,kind) = c let declare_constant ?(internal = UserVerbose) id (cd,kind) = - let cd = hcons_constant_declaration cd in let kn = declare_constant_common id [] (ConstantEntry cd,kind) in !xml_declare_constant (internal,kn); kn |