diff options
| author | Pierre-Marie Pédrot | 2017-09-10 02:21:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-28 16:51:21 +0200 |
| commit | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (patch) | |
| tree | 16dc8bc2ae1b5374a1329b9f6495d0a1b9905ee4 /plugins | |
| parent | d28304f6ba18ad9527a63cd01b39a5ad27526845 (diff) | |
Efficient computation of the names contained in an environment.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/evar_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index be1d947d3c..d9150a7bbd 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 (Context.Named.to_vars (Environ.named_context env)) + Namegen.next_ident_away_in_goal id (Termops.vars_of_env env) | Name.Name id -> id in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in |