aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorMatej Kosik2016-02-15 19:11:42 +0100
committerMatej Kosik2016-02-15 19:11:42 +0100
commit97d6583a0b9a65080639fb02deba4200f6276ce6 (patch)
tree7e3407649be5fc1f9d47c891b0591ffd4e468468 /kernel/nativelambda.ml
parent5180ab68819f10949cd41a2458bff877b3ec3204 (diff)
parent4f041384cb27f0d24fa14b272884b4b7f69cacbe (diff)
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r--kernel/nativelambda.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 01f59df15a..91b40be7e9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -727,7 +727,8 @@ let optimize lam =
let lambda_of_constr env sigma c =
set_global_env env;
let env = Renv.make () in
- let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
+ let open Context.Rel.Declaration in
+ let ids = List.rev_map get_name !global_env.env_rel_context 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