Taking current env and not global env in b286c9f (4 commits ago,

as revealed by rocq-prover#2141).

Author: herbelin

pretyping/retyping.ml

@@ -109,7 +109,7 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in
+        let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
         let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))