Replacing Id.check with Id.is_valid, as its sole use was under

an ugly try ... with construct.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16516 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 12 insertions, 25 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 87249dec10..fbd26ca3d8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -38,9 +38,9 @@ struct
     in
     Option.iter iter (Unicode.ident_refutation x)
 
-  let check x =
-    let iter (_, x) = Errors.error x in
-    Option.iter iter (Unicode.ident_refutation x)
+  let is_valid s = match Unicode.ident_refutation s with
+  | None -> true
+  | Some _ -> false
 
   let of_string s =
     let () = check_soft s in
@@ -630,8 +630,6 @@ type identifier = Id.t
 
 let id_eq = Id.equal
 let id_ord = Id.compare
-let check_ident_soft = Id.check_soft
-let check_ident = Id.check
 let string_of_id = Id.to_string
 let id_of_string = Id.of_string
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 4b20b1c73a..c2409649c0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -19,17 +19,12 @@ sig
   val compare : t -> t -> int
   (** Comparison over identifiers *)
 
-  val check : string -> unit
-  (** Check that a string may be converted to an identifier.
-      Raise a [UserError _] exception related to the problem
-      when this is not the case. *)
-
-  val check_soft : string -> unit
-  (** As [check], but may raise a warning instead of failing when the string is
-      not an identifier, but is a well-formed string. *)
+  val is_valid : string -> bool
+  (** Check that a string may be converted to an identifier. *)
 
   val of_string : string -> t
-  (** Converts a string into an identifier. May raise [UserError _] *)
+  (** Converts a string into an identifier. May raise [UserError _] if the
+      string is not valid. *)
 
   val to_string : t -> string
   (** Converts a identifier into an string. *)
@@ -439,12 +434,6 @@ val eq_ind_chk : inductive -> inductive -> bool
 type identifier = Id.t
 (** @deprecated Alias for [Id.t] *)
 
-val check_ident : string -> unit
-(** @deprecated Same as [Id.check]. *)
-
-val check_ident_soft : string -> unit
-(** @deprecated Same as [Id.check_soft]. *)
-
 val string_of_id : identifier -> string
 (** @deprecated Same as [Id.to_string]. *)
 
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 5413e69a0c..f55a12f9d4 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -74,8 +74,10 @@ let scheme_object_table =
   (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
 
 let declare_scheme_object s aux f =
-  (try Id.check ("ind"^s) with UserError _ ->
-    error ("Illegal induction scheme suffix: "^s));
+  let () =
+    if not (Id.is_valid ("ind" ^ s)) then
+      error ("Illegal induction scheme suffix: " ^ s)
+  in
   let key = if String.is_empty aux then s else aux in
   try
     let _ = Hashtbl.find scheme_object_table key in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b1a1cf03c6..d7d6bc8f1d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1472,13 +1472,11 @@ let interp_search_restriction = function
 
 open Search
 
-let is_ident s = try ignore (Id.check s); true with UserError _ -> false
-
 let interp_search_about_item = function
   | SearchSubPattern pat ->
       let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in
       GlobSearchSubPattern pat
-  | SearchString (s,None) when is_ident s ->
+  | SearchString (s,None) when Id.is_valid s ->
       GlobSearchString s
   | SearchString (s,sc) ->
       try