Move type definition Nativecode.symbols to Nativevalues

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

1 files changed, 17 insertions, 0 deletions

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 *)