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.mli | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'kernel/nativevalues.mli')

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