diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 27 |
1 files changed, 3 insertions, 24 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index d57dd7b40d..5c30f05aae 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -336,18 +336,7 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let _ = - declare_bool_option - { optsync = true; - optname = "automatic importation of coercions"; - optkey = ["Automatic";"Coercions";"Importation"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } - -let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) = +let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) = add_class cls; add_class clt; let is,_ = class_info cls in @@ -361,17 +350,8 @@ let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) = add_new_coercion coe xf; add_coercion_in_graph (xf,is,it) -let load_coercion _ o = - if - !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2 - then - cache_coercion o - -let open_coercion _ o = - if not - (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) - then - cache_coercion o +let cache_coercion o = + load_coercion 1 o let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) = let coe' = subst_coe_typ subst coe in @@ -400,7 +380,6 @@ let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = let (inCoercion,_) = declare_object {(default_object "COERCION") with - open_function = open_coercion; load_function = load_coercion; cache_function = cache_coercion; subst_function = subst_coercion; |