diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /kernel/nativecode.mli | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'kernel/nativecode.mli')
| -rw-r--r-- | kernel/nativecode.mli | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 893db92d..5d4c9e1e 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit val mk_open : string -> global +(* Precomputed values for a compilation unit *) type symbol +type symbols -val clear_symb_tbl : unit -> unit +val empty_symbols : symbols -val get_value : symbol array -> int -> Nativevalues.t +val clear_symbols : unit -> unit -val get_sort : symbol array -> int -> sorts +val get_value : symbols -> int -> Nativevalues.t -val get_name : symbol array -> int -> name +val get_sort : symbols -> int -> sorts -val get_const : symbol array -> int -> constant +val get_name : symbols -> int -> name -val get_match : symbol array -> int -> Nativevalues.annot_sw +val get_const : symbols -> int -> constant -val get_ind : symbol array -> int -> inductive +val get_match : symbols -> int -> Nativevalues.annot_sw -val get_meta : symbol array -> int -> metavariable +val get_ind : symbols -> int -> inductive -val get_evar : symbol array -> int -> existential +val get_meta : symbols -> int -> metavariable -val get_level : symbol array -> int -> Univ.Level.t +val get_evar : symbols -> int -> existential -val get_symbols_tbl : unit -> symbol array +val get_level : symbols -> int -> Univ.Level.t + +val get_symbols : unit -> symbols type code_location_update type code_location_updates |