[env.env_rel_context.env_rel_ctx] -> [rel_context env]

It's a bit shorter and more direct.

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 74d12f3cd..1748e98a4 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1845,7 +1845,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
   in
   let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
   let auxdefs = List.fold_right get_named_val fv_named auxdefs in
-  let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in
+  let lvl = Context.Rel.length (rel_context env) in
   let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
   let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
   let aux_name = fresh_lname Anonymous in
@@ -1854,7 +1854,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
 and compile_rel env sigma univ auxdefs n =
   let open Context.Rel.Declaration in
   let decl = lookup_rel n env in
-  let n = List.length env.env_rel_context.env_rel_ctx - n in
+  let n = List.length (rel_context env) - n in
   match decl with
   | LocalDef (_,t,_) ->
       let code = lambda_of_constr env sigma t in