diff options
Diffstat (limited to 'kernel/nativecode.mli')
-rw-r--r-- | kernel/nativecode.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f8..684983a87 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -10,7 +10,7 @@ open Names open Constr open Declarations -open Pre_env +open Environ open Nativelambda (** This file defines the mllambda code generation phase of the native @@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t +val get_proj : symbols -> int -> inductive * int + val get_symbols : unit -> symbols type code_location_update |