Merge PR #7234: Reduce circular dependency constants <-> projections

1 files changed, 1 insertions, 3 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bed598bb7..090acdf16e 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