diff options
| author | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /kernel/nativecode.mli | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
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 893db92dd8..5d4c9e1e2d 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 |