Move type definition Nativecode.symbols to Nativevalues

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

1 files changed, 0 insertions, 16 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