diff options
Diffstat (limited to 'tactics/decl_interp.ml')
| -rw-r--r-- | tactics/decl_interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index bfb5039d5..2b583af40 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -223,7 +223,7 @@ let rec deanonymize ids = function PatVar (loc,Anonymous) -> let (found,known) = !ids in - let new_id=Nameops.next_ident_away dummy_prefix known in + let new_id=Namegen.next_ident_away dummy_prefix known in let _= ids:= (loc,new_id) :: found , new_id :: known in PatVar (loc,Name new_id) | PatVar (loc,Name id) as pat -> |