diff options
author | 2009-11-09 18:05:13 +0000 | |
---|---|---|
committer | 2009-11-09 18:05:13 +0000 | |
commit | 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 (patch) | |
tree | fc18af5b3330e830a8e979bc551db46b25bda05d /tactics/decl_interp.ml | |
parent | cb2f5d06481f9021f600eaefbdc6b33118bd346d (diff) |
A bit of cleaning around name generation + creation of dedicated file namegen.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
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 -> |