diff options
| author | ppedrot | 2012-12-13 16:00:06 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-13 16:00:06 +0000 |
| commit | 02077f5b5e132e135be778c201e74a5eb87b97ae (patch) | |
| tree | f98da56fa4cdcd5cb5ea0e1f193c2f84d687feb5 /interp | |
| parent | 0a7347b567d6ea5d71907b570c81ea6dc61a626d (diff) | |
Using library string functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 ^ "_" ^ |