From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 kernel/nativelambda.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index a5cdd0a19c..cec0ee57d5 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -464,10 +464,9 @@ let rec lambda_of_constr cache env sigma c =
   | Construct _ ->  lambda_of_app cache env sigma c empty_args
 
   | Proj (p, c) ->
-    let pb = lookup_projection p env in
-    let ind = pb.proj_ind in
+    let ind = Projection.inductive p in
     let prefix = get_mind_prefix env (fst ind) in
-    mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr cache env sigma c|]
+    mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in
-- 
cgit v1.2.3