diff options
| author | letouzey | 2007-10-25 16:21:14 +0000 |
|---|---|---|
| committer | letouzey | 2007-10-25 16:21:14 +0000 |
| commit | 6c747d9e923406a124820a30ff06076cec43215d (patch) | |
| tree | 8b0dc81452ea6b2f40da52f9c678409d6f9ae1d1 | |
| parent | 7156868c56b1a1cea0fde1889db087f3308f3f5d (diff) | |
small fix of commit 10188: a string given via Extract Inductive can be empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10266 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/ocaml.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 3326544a1c..f3df9230d0 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -95,7 +95,9 @@ let pp_modname mp = str (Common.pp_module mp) let is_infix r = is_inline_custom r && - (let s = find_custom r in s.[0] = '(' && s.[String.length s-1] = ')') + (let s = find_custom r in + let l = String.length s in + l >= 2 && s.[0] = '(' && s.[l-1] = ')') let get_infix r = let s = find_custom r in |