diff options
| author | Maxime Dénès | 2013-12-28 20:39:17 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2013-12-28 20:39:17 -0500 |
| commit | d3eac3d5fc8e5af499eb8750ca08ead8562dac6f (patch) | |
| tree | 70540c3d5e8b0856db2a9e82710e1b32cdc8465d /kernel/environ.mli | |
| 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/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 38a1bf68a1..66cb03a1cd 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -117,6 +117,8 @@ val reset_with_named_context : named_context_val -> env -> env {6 Add entries to global environment } *) val add_constant : constant -> constant_body -> env -> env +val add_constant_key : constant -> constant_body -> Pre_env.link_info ref -> + env -> env (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) @@ -136,7 +138,7 @@ val constant_type : env -> constant -> constant_type val constant_opt_value : env -> constant -> constr option (** {5 Inductive types } *) - +val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names @@ -229,4 +231,5 @@ val unregister : env -> field -> env val register : env -> field -> Retroknowledge.entry -> env - +(** Native compiler *) +val no_link_info : unit -> Pre_env.link_info ref |