Reverted 13293 commited mistakenly. Sorry for the noise.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7

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;