diff options
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 |