From c4486dfda07b872d20746778df5c443b052b92b9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 9 Jul 2015 21:08:44 +0200
Subject: Native compiler: refactor code handling pre-computed values.

Fixes #4139 (Not_found exception with Require in modules).
---
 kernel/nativecode.mli | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

(limited to 'kernel/nativecode.mli')

diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 893db92dd8..5d4c9e1e2d 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit
 
 val mk_open : string -> global
 
+(* Precomputed values for a compilation unit *)
 type symbol
+type symbols
 
-val clear_symb_tbl : unit -> unit
+val empty_symbols : symbols
 
-val get_value : symbol array -> int -> Nativevalues.t
+val clear_symbols : unit -> unit
 
-val get_sort : symbol array -> int -> sorts
+val get_value : symbols -> int -> Nativevalues.t
 
-val get_name : symbol array -> int -> name
+val get_sort : symbols -> int -> sorts
 
-val get_const : symbol array -> int -> constant
+val get_name : symbols -> int -> name
 
-val get_match : symbol array -> int -> Nativevalues.annot_sw
+val get_const : symbols -> int -> constant
 
-val get_ind : symbol array -> int -> inductive
+val get_match : symbols -> int -> Nativevalues.annot_sw
 
-val get_meta : symbol array -> int -> metavariable
+val get_ind : symbols -> int -> inductive
 
-val get_evar : symbol array -> int -> existential
+val get_meta : symbols -> int -> metavariable
 
-val get_level : symbol array -> int -> Univ.Level.t
+val get_evar : symbols -> int -> existential
 
-val get_symbols_tbl : unit -> symbol array
+val get_level : symbols -> int -> Univ.Level.t
+
+val get_symbols : unit -> symbols
 
 type code_location_update
 type code_location_updates
-- 
cgit v1.2.3