From c7bd285555153294ec077cfa05c36bb420716f3b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 12 Apr 2018 21:41:03 +0200 Subject: Reduce circular dependency constants <-> projections Instead of having the projection data in the constant data we have it independently in the environment. --- kernel/inductive.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb..090acdf16 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -803,9 +803,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 kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code -- cgit v1.2.3