From 793a442d240c22f99591388ad31e33fbaef96fb0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 11 Jun 2019 11:22:24 +0200
Subject: Move type definition Nativecode.symbols to Nativevalues

Preparing for it to be stored in an Environ.env.
---
 kernel/nativevalues.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'kernel/nativevalues.ml')

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 *)
-- 
cgit v1.2.3