Using library string functions.

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

8 files changed, 12 insertions, 12 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 3bbc14038e..f74031687c 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -205,7 +205,7 @@ EXTEND
         let t, g = interp_entry_name false None e sep in
         GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
       | s = STRING ->
-	if String.equal s "" then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
+	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
         GramTerminal s
     ] ]
   ;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 321cacbf71..29a59da79f 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -84,7 +84,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
         ->
-      if String.equal s "" then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
+      if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
       (Some s,l,<:expr< fun () -> $e$ >>)
       | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
 	  (None,l,<:expr< fun () -> $e$ >>)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e237583d72..72577d8664 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -293,8 +293,8 @@ let drop_implicits_in_patt cst nb_expl args =
        impls_fit [] (imps,args)
 
 let has_curly_brackets ntn =
-  String.length ntn >= 6 && (String.equal (String.sub ntn 0 6) "{ _ } " ||
-    String.equal (String.sub ntn (String.length ntn - 6) 6) " { _ }" ||
+  String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 ||
+    String.is_sub " { _ }" ntn (String.length ntn - 6) ||
     String.string_contains ~where:ntn ~what:" { _ } ")
 
 let rec wildcards ntn n =
@@ -312,7 +312,7 @@ let expand_curly_brackets loc mknot ntn l =
     | a::l ->
         let a' =
           let p = List.nth (wildcards !ntn' 0) i - 2 in
-          if p>=0 & p+5 <= String.length !ntn' && String.equal (String.sub !ntn' p 5) "{ _ }"
+          if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p
           then begin
             ntn' :=
               String.sub !ntn' 0 p ^ "_" ^
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3d0790564c..a05ce24156 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2276,7 +2276,7 @@ let make_up_names n ind_opt cname =
   id_of_string base, hyprecname, avoid
 
 let error_ind_scheme s =
-  let s = if not (String.equal s "") then s^" " else s in
+  let s = if not (String.is_empty s) then s^" " else s in
   error ("Cannot recognize "^s^"an induction scheme.")
 
 let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b104ef4c88..00875a6812 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -63,11 +63,11 @@ let remove_top_ml () = Mltop.remove ()
 
 let inputstate = ref ""
 let set_inputstate s = inputstate:=s
-let inputstate () = if not (String.equal !inputstate "") then intern_state !inputstate
+let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate
 
 let outputstate = ref ""
 let set_outputstate s = outputstate:=s
-let outputstate () = if not (String.equal !outputstate "") then extern_state !outputstate
+let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
 
 let set_default_include d = push_include (d,Nameops.default_root_prefix)
 let set_include d p =
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 44b87b0c68..9cbf5c1ceb 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -89,7 +89,7 @@ let scheme_object_table =
 let declare_scheme_object s aux f =
   (try check_ident ("ind"^s) with _ ->
     error ("Illegal induction scheme suffix: "^s));
-  let key = if String.equal aux "" then s else aux in
+  let key = if String.is_empty aux then s else aux in
   try
     let _ = Hashtbl.find scheme_object_table key in
 (*    let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 53876134b9..71305cb134 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -261,7 +261,7 @@ let parse_format ((loc, str) : lstring) =
     else push_white n [[]]
   in
   try
-    if not (String.equal str "") then match parse_token 0 with
+    if not (String.is_empty str) then match parse_token 0 with
       | [l] -> l
       | _ -> error "Box closed without being opened in format."
     else
@@ -1083,7 +1083,7 @@ let contract_notation ntn =
   let rec aux ntn i =
     if i <= String.length ntn - 5 then
       let ntn' =
-        if String.equal (String.sub ntn i 5) "{ _ }" then
+        if String.is_sub "{ _ }" ntn i then
           String.sub ntn 0 i ^ "_" ^
           String.sub ntn (i+5) (String.length ntn -i-5)
         else ntn in
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 3a99d9df94..435258720c 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -228,7 +228,7 @@ let make_emacs_prompt() =
   let pending = Pfedit.get_all_proof_names() in
   let pendingprompt =
     List.fold_left
-      (fun acc x -> acc ^ (if String.equal acc "" then "" else "|") ^ Names.string_of_id x)
+      (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.string_of_id x)
       "" pending in
   let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
   if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "