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

2 files changed, 7 insertions, 20 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]. *)