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/nativecode.ml | 16 ----------------
 1 file changed, 16 deletions(-)

(limited to 'kernel/nativecode.ml')

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