From 1847057e19e518fd8ab87ead5d7fdd006dfa0367 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Nov 2008 21:27:50 +0000
Subject: Adaptation to ocaml 3.11 new semantics of String.index_from (see bug
 #1974) Grant wish #1988 ("fun" forces reduction in "refine" if needed)

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

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 9428aa134d..7df7063930 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -83,6 +83,9 @@ let rec is_sub gdzie gl gi co cl ci =
    (is_sub gdzie gl (gi+1) co cl (ci+1)))
 
 let rec raw_str_index i gdzie l c co cl = 
+  (* First adapt to ocaml 3.11 new semantics of index_from *)
+  if (i+cl > l) then raise Not_found;
+  (* Then proceed as in ocaml < 3.11 *)
   let i' = String.index_from gdzie i c in
     if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
       raw_str_index (i'+1) gdzie l c co cl
-- 
cgit v1.2.3