From a8c4dee491fdd2426c623ad458ed15310295c93b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 18 Jun 2018 14:05:09 +0200
Subject: [env.env_rel_context.env_rel_ctx] -> [rel_context env]

It's a bit shorter and more direct.
---
 kernel/clambda.ml      | 2 +-
 kernel/nativecode.ml   | 4 ++--
 kernel/nativelambda.ml | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index b722e4200..f1b6f3dff 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -814,7 +814,7 @@ let optimize_lambda lam =
 
 let lambda_of_constr ~optimize genv c =
   let env = Renv.make genv in
-  let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in
+  let ids = List.rev_map Context.Rel.Declaration.get_name (rel_context genv) in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env c in
   let lam = if optimize then optimize_lambda lam else lam in
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
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 244e5e0dd..5843cd543 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -659,7 +659,7 @@ let optimize lam =
 let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
-  let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context.env_rel_ctx in
+  let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin
-- 
cgit v1.2.3