aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/evar_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/evar_tactics.ml')
-rw-r--r--plugins/ltac/evar_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 4cab6ef33..be1d947d3 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -88,7 +88,7 @@ let let_evar name typ =
let id = match name with
| Name.Anonymous ->
let id = Namegen.id_of_name_using_hdchar env sigma typ name in
- Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
+ Namegen.next_ident_away_in_goal id (Context.Named.to_vars (Environ.named_context env))
| Name.Name id -> id
in
let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in