From 02077f5b5e132e135be778c201e74a5eb87b97ae Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 13 Dec 2012 16:00:06 +0000
Subject: Using library string functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16065 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

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 ^ "_" ^
-- 
cgit v1.2.3