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/csymtable.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/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 146b6a1ec..0111cf74d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -92,7 +92,7 @@ let slot_for_annot key = n let rec slot_for_getglobal env kn = - let (cb,rk) = lookup_constant_key kn env in + let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) |