From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 library/nameops.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'library/nameops.ml')

diff --git a/library/nameops.ml b/library/nameops.ml
index 779f3389..6d0ad8ef 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml 9225 2006-10-09 15:59:23Z herbelin $ *)
+(* $Id: nameops.ml 9429 2006-12-12 08:01:03Z herbelin $ *)
 
 open Pp
 open Util
@@ -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)
 
-- 
cgit v1.2.3