From 5458617d1b3c6b0a5ff846ef977d3bdaeda9fb4f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Dec 2006 09:38:53 +0000
Subject: Correction bug #1041 (double cause : non évitement des noms existants
 en cas de création de nom par défaut; utilisation de _ comme nom dans
 evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar +
 essai de ne pas faire dépendre les evars des variables anonymes afin   de
 résoudre le bug #932

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/nameops.ml  | 7 +------
 library/nameops.mli | 2 --
 2 files changed, 1 insertion(+), 8 deletions(-)

(limited to 'library')

diff --git a/library/nameops.ml b/library/nameops.ml
index b68c095936..6c5000dfef 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -20,8 +20,6 @@ let pr_name = function
   | Anonymous -> str "_"
   | Name id -> pr_id id
 
-let wildcard = id_of_string "_"
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -163,10 +161,7 @@ let next_name_away_with_default default name l =
     | Name str  -> next_ident_away str l
     | Anonymous -> next_ident_away (id_of_string default) l
 
-let next_name_away name l = 
-  match name with
-    | Name str  -> next_ident_away str l
-    | Anonymous -> id_of_string "_"
+let next_name_away = next_name_away_with_default "H"
 
 let pr_lab l = str (string_of_label l)
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 895513a3c0..336099a2ff 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -14,8 +14,6 @@ open Names
 val pr_id : identifier -> Pp.std_ppcmds
 val pr_name : name -> Pp.std_ppcmds
 
-val wildcard : identifier
-
 val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option
 
-- 
cgit v1.2.3