From d3eac3d5fc8e5af499eb8750ca08ead8562dac6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 28 Dec 2013 20:39:17 -0500
Subject: 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.
---
 kernel/csymtable.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 146b6a1ec9..0111cf74db 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");*)
-- 
cgit v1.2.3