diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 282f181ebb..9fd94c75b8 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -342,8 +342,8 @@ open Goptions let _ = declare_bool_option { optsync = true; - optname = "automatic importation of coercions"; - optkey = ["Automatic";"Coercions";"Importation"]; + optname = "automatic import of coercions"; + optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } |