From e1e7888ac4519f4b7470cc8469f9fd924514e352 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Jun 2018 17:30:14 +0200 Subject: More straightforward native compilation of primitive projections. Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain. --- kernel/nativecode.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/nativecode.mli') diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 42f2cbc2e..684983a87 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -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 -- cgit v1.2.3