diff options
| author | Gaëtan Gilbert | 2019-06-11 11:22:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 11:22:24 +0200 |
| commit | 793a442d240c22f99591388ad31e33fbaef96fb0 (patch) | |
| tree | 1479c5e61cb174356bc5deea2f6ec64b05f21036 /kernel/nativevalues.mli | |
| parent | 45306c6c9c433b86406d041f58aafb7cf3a3ff82 (diff) | |
Move type definition Nativecode.symbols to Nativevalues
Preparing for it to be stored in an Environ.env.
Diffstat (limited to 'kernel/nativevalues.mli')
| -rw-r--r-- | kernel/nativevalues.mli | 16 |
1 files changed, 16 insertions, 0 deletions
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 |