diff options
| author | Jason Gross | 2014-08-12 11:14:04 -0400 |
|---|---|---|
| committer | Pierre Boutillier | 2014-08-25 15:22:40 +0200 |
| commit | 4fef230a1ee1964712e3ac7f325ce00968ac4769 (patch) | |
| tree | 7be49300bc9c989a4ec716685356cb8f5aab752e /ide | |
| parent | 876b1b39a0304c93c2511ca8dd34353413e91c9d (diff) | |
"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).
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/utils/config_file.mli | 4 | ||||
| -rw-r--r-- | ide/utils/configwin_ihm.ml | 2 |
3 files changed, 4 insertions, 4 deletions
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 |