diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 01f59df15..91b40be7e 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 |