diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 03ae6e763..fe4d0f300 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -349,6 +349,7 @@ open Goptions let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic import of coercions"; optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); |