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