From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/nativecode.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/nativecode.mli') diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f..96efa7fa 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 @@ -65,7 +67,7 @@ val register_native_file : string -> unit val compile_constant_field : env -> string -> Constant.t -> global list -> constant_body -> global list -val compile_mind_field : string -> ModPath.t -> Label.t -> +val compile_mind_field : ModPath.t -> Label.t -> global list -> mutual_inductive_body -> global list val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code -- cgit v1.2.3