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/inductive.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 88b00600e4..4d13a5fcb8 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -798,8 +798,7 @@ let rec subterm_specif renv stack t =
          (* We take the subterm specs of the constructor of the record *)
          let wf_args = (dest_subterms wf).(0) in
          (* We extract the tree of the projected argument *)
-         let pb = lookup_projection p renv.env in
-         let n = pb.proj_arg in
+         let n = Projection.arg p in
          spec_of_tree (List.nth wf_args n)
        | Dead_code -> Dead_code
        | Not_subterm -> Not_subterm)
-- 
cgit v1.2.3