aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r--kernel/nativelambda.ml2
1 files changed, 1 insertions, 1 deletions
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