Move type definition Nativecode.symbols to Nativevalues

Preparing for it to be stored in an Environ.env.

8 files changed, 40 insertions, 27 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 3f791dfc22..347fdc773d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -141,18 +141,6 @@ let fresh_gnormtbl l =
 
 (** Symbols (pre-computed values) **)
 
-type symbol =
-  | SymbValue of Nativevalues.t
-  | SymbSort of Sorts.t
-  | SymbName of Name.t
-  | SymbConst of Constant.t
-  | SymbMatch of annot_sw
-  | SymbInd of inductive
-  | SymbMeta of metavariable
-  | SymbEvar of Evar.t
-  | SymbLevel of Univ.Level.t
-  | SymbProj of (inductive * int)
-
 let dummy_symb = SymbValue (dummy_value ())
 
 let eq_symbol sy1 sy2 =
@@ -194,10 +182,6 @@ let symb_tbl = HashtblSymbol.create 211
 
 let clear_symbols () = HashtblSymbol.clear symb_tbl
 
-type symbols = symbol array
-
-let empty_symbols = [||]
-
 let get_value tbl i =
   match tbl.(i) with
     | SymbValue v -> v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index b5c03b6ca3..caebbc63a6 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -12,6 +12,7 @@ open Constr
 open Declarations
 open Environ
 open Nativelambda
+open Nativevalues
 
 (** This file defines the mllambda code generation phase of the native
 compiler. mllambda represents a fragment of ML, and can easily be printed
@@ -25,11 +26,6 @@ val pp_global : Format.formatter -> global -> unit
 val mk_open : string -> global
 
 (* Precomputed values for a compilation unit *)
-type symbol
-type symbols
-
-val empty_symbols : symbols
-
 val clear_symbols : unit -> unit
 
 val get_value : symbols -> int -> Nativevalues.t
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 31e5255fc4..1485e97b47 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -16,4 +16,4 @@ open Nativecode
 compiler *)
 
 val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
-  global list * symbols
+  global list * Nativevalues.symbols
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 3eb51ffc59..1102dd6cae 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -66,6 +66,23 @@ type atom =
   | Aevar of Evar.t * t array
   | Aproj of (inductive * int) * accumulator
 
+type symbol =
+  | SymbValue of t
+  | SymbSort of Sorts.t
+  | SymbName of Name.t
+  | SymbConst of Constant.t
+  | SymbMatch of annot_sw
+  | SymbInd of inductive
+  | SymbMeta of metavariable
+  | SymbEvar of Evar.t
+  | SymbLevel of Univ.Level.t
+  | SymbProj of (inductive * int)
+
+type symbols = symbol array
+
+let empty_symbols = [| |]
+
+
 let accumulate_tag = 0
 
 (** Unique pointer used to drive the accumulator function *)
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 58cb6e2c30..c037d2bde7 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -56,6 +56,22 @@ type atom =
   | Aevar of Evar.t * t array (* arguments *)
   | Aproj of (inductive * int) * accumulator
 
+type symbol =
+  | SymbValue of t
+  | SymbSort of Sorts.t
+  | SymbName of Name.t
+  | SymbConst of Constant.t
+  | SymbMatch of annot_sw
+  | SymbInd of inductive
+  | SymbMeta of metavariable
+  | SymbEvar of Evar.t
+  | SymbLevel of Univ.Level.t
+  | SymbProj of (inductive * int)
+
+type symbols = symbol array
+
+val empty_symbols : symbols
+
 (* Constructors *)
 
 val mk_accu : atom -> t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 824400b4e3..2284196efe 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -130,7 +130,7 @@ type safe_environment =
     required : vodigest DPMap.t;
     loads : (ModPath.t * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
-    native_symbols : Nativecode.symbols DPMap.t }
+    native_symbols : Nativevalues.symbols DPMap.t }
 
 and modvariant =
   | NONE
@@ -1076,7 +1076,7 @@ type compiled_library = {
   comp_mod : module_body;
   comp_deps : library_info array;
   comp_enga : engagement;
-  comp_natsymbs : Nativecode.symbols
+  comp_natsymbs : Nativevalues.symbols
 }
 
 let module_of_library lib = lib.comp_mod
@@ -1128,7 +1128,7 @@ let export ?except ~output_native_objects senv dir =
   let ast, symbols =
     if output_native_objects then
       Nativelibrary.dump_library mp dir senv.env str
-    else [], Nativecode.empty_symbols
+    else [], Nativevalues.empty_symbols
   in
   let lib = {
     comp_name = dir;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 770caf5406..d8f7f0cc40 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -179,7 +179,7 @@ type native_library = Nativecode.global list
 
 val module_of_library : compiled_library -> Declarations.module_body
 
-val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
+val get_library_native_symbols : safe_environment -> DirPath.t -> Nativevalues.symbols
 
 val start_library : DirPath.t -> ModPath.t safe_transformer
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 2b28ba908e..c35abae155 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -94,7 +94,7 @@ val register_library :
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
   Univ.ContextSet.t -> unit
 
-val get_library_native_symbols : library_name -> Nativecode.symbols
+val get_library_native_symbols : library_name -> Nativevalues.symbols
 
 val start_library : library_name -> unit