Fix #8873: coqchk on inductive with letin parameter

1 files changed, 4 insertions, 3 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 50e65ef587..f6c510ee1c 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -531,10 +531,11 @@ let check_positivity env_ar mind params nrecp inds =
     Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
+  let ra_env =
+    List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
+  let env_ar_par = push_rel_context params env_ar in
   let check_one i mip =
-    let ra_env =
-      List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
-    let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
+    let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in
       check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
   let irecargs = Array.mapi check_one inds in