aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 32da81f96..9a973cff5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,8 +428,7 @@ let automatically_import_coercions = ref false
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic import of coercions";
optkey = ["Automatic";"Coercions";"Import"];
optread = (fun () -> !automatically_import_coercions);
@@ -556,7 +555,6 @@ module CoercionPrinting =
let member_message x b =
str "Explicit printing of coercion " ++ printer x ++
str (if b then " is set" else " is unset")
- let synchronous = true
end
module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting)