From 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 9 Nov 2009 18:05:13 +0000
Subject: 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
---
 tactics/decl_interp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/decl_interp.ml')

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 ->
-- 
cgit v1.2.3