From e1e7888ac4519f4b7470cc8469f9fd924514e352 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/nativevalues.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativevalues.ml')

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index cfcb0a485..da4413a0a 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -64,7 +64,7 @@ type atom =
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
   | Aevar of Evar.t * t * t array
-  | Aproj of Constant.t * accumulator
+  | Aproj of (inductive * int) * accumulator
 
 let accumulate_tag = 0
 
-- 
cgit v1.2.3