From 4fef230a1ee1964712e3ac7f325ce00968ac4769 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 12 Aug 2014 11:14:04 -0400
Subject: "allows to", like "allowing to", is improper

It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
---
 ide/coqide.ml              | 2 +-
 ide/utils/config_file.mli  | 4 ++--
 ide/utils/configwin_ihm.ml | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'ide')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index b0d90f2cbd..ba20c771a6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1377,7 +1377,7 @@ let check_for_geoproof_input () =
     full name, with the last occurrence of "coqide" replaced by "coqtop".
     This should correctly handle the ".opt", ".byte", ".exe" situations.
     If the replacement fails, we default to "coqtop", hoping it's somewhere
-    in the path. Note that the -coqtop option to coqide allows to override
+    in the path. Note that the -coqtop option to coqide overrides
     this default coqtop path *)
 
 let read_coqide_args argv =
diff --git a/ide/utils/config_file.mli b/ide/utils/config_file.mli
index b9c7768280..22328e7f1f 100644
--- a/ide/utils/config_file.mli
+++ b/ide/utils/config_file.mli
@@ -141,8 +141,8 @@ exception Missing_cp of groupable_cp
 or used to generate command line arguments.
 
 The basic usage is to have only one group and one configuration file,
-but this mechanism allows to have more,
-for instance to have another smaller group for the options to pass on the command line.
+but this mechanism allows having more,
+for instance having another smaller group for the options to pass on the command line.
 *)
 class group : object
   (** Adds a cp to the group.
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index ad12ad5fdb..c1062a9db1 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -67,7 +67,7 @@ let html_config_file_and_option () =
 let last_dir = ref "";;
 
 (** This function allows the user to select a file and returns the
-   selected file name. An optional function allows to change the
+   selected file name. An optional function allows changing the
    behaviour of the ok button.
    A VOIR : mutli-selection ? *)
 let select_files ?dir
-- 
cgit v1.2.3