aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-15 11:52:19 +0200
committerMaxime Dénès2017-06-15 11:52:19 +0200
commit28c732ea340f5ac571a77a8ac26de600c29165b2 (patch)
tree9ee6deb6ecb31c520ffb4c278560a527cb550db4 /pretyping/classops.ml
parente710306910afc61c9a874e6020bbf35b77ffe4af (diff)
parent7668037a8daaef7bc8f1fc3225c2e6cc26cac0aa (diff)
Merge PR#375: Deprecation
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml10
1 files changed, 3 insertions, 7 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9a973cff55..8d87f6e99c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,7 +428,7 @@ let automatically_import_coercions = ref false
open Goptions
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "automatic import of coercions";
optkey = ["Automatic";"Coercions";"Import"];
optread = (fun () -> !automatically_import_coercions);
@@ -454,15 +454,11 @@ let cache_coercion (_, c) =
add_coercion_in_graph (xf,is,it)
let load_coercion _ o =
- if
- !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2
- then
+ if !automatically_import_coercions then
cache_coercion o
let open_coercion i o =
- if Int.equal i 1 && not
- (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
- then
+ if Int.equal i 1 && not !automatically_import_coercions then
cache_coercion o
let subst_coercion (subst, c) =