aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/sentence.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:50:02 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:50:02 +0100
commit2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e (patch)
treed36a8ce954b3fb4d3ba0f0b93ca80816620654fc /ide/sentence.ml
parenta5e1b40b93e47a278746ee6752474891cd856c29 (diff)
Remove useless rec flags.
Diffstat (limited to 'ide/sentence.ml')
-rw-r--r--ide/sentence.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/sentence.ml b/ide/sentence.ml
index dd6b10a46..8195051c6 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -63,13 +63,13 @@ let grab_sentence_start (iter:GText.iter) soi =
(** Search forward the first character immediately after a sentence end *)
-let rec grab_sentence_stop (start:GText.iter) =
+let grab_sentence_stop (start:GText.iter) =
(forward_search is_sentence_end start)#forward_char
(** Search forward the first character immediately after a "." sentence end
(and not just a "\{" or "\}" or comment end *)
-let rec grab_ending_dot (start:GText.iter) =
+let grab_ending_dot (start:GText.iter) =
let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
(forward_search is_ending_dot start)#forward_char