diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2013-12-28 20:39:17 -0500 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2013-12-28 20:39:17 -0500 |
| commit | d3eac3d5fc8e5af499eb8750ca08ead8562dac6f (patch) | |
| tree | 70540c3d5e8b0856db2a9e82710e1b32cdc8465d /kernel/declareops.ml | |
| parent | a681e57e3c76dff2fe710ce533179ea659d8de0b (diff) | |
Removing native_name reference from constant_body.
For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 724f29092..2e691491a 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -65,7 +65,6 @@ let subst_const_body sub cb = { const_type = subst_const_type sub cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; const_constraints = cb.const_constraints; - const_native_name = ref NotLinked; const_inline_code = cb.const_inline_code } (** {7 Hash-consing of constants } *) @@ -201,8 +200,7 @@ let subst_mind sub mib = else { mib with mind_params_ctxt = params'; - mind_packets = packets'; - mind_native_name = ref NotLinked } + mind_packets = packets' } (** {6 Hash-consing of inductive declarations } *) |