Made coercions active only when modules are imported.

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

2 files changed, 25 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 1d90d85ba..e43228ef3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -131,6 +131,7 @@ Module system
 - A functor application can be prefixed by a "!" to make it ignore any
   "Inline" annotation in the type of its argument(s) (for examples of
   use of the new features, see libraries Structures and Numbers).
+- Coercions are now active only when modules are imported.
 
 Extraction
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5c30f05aa..282f181eb 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -336,7 +336,18 @@ let class_params = function
 let add_class cl =
   add_new_class cl { cl_param = class_params cl }
 
-let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
+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)) =
   add_class cls;
   add_class clt;
   let is,_ = class_info cls in
@@ -350,8 +361,17 @@ let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
   add_new_coercion coe xf;
   add_coercion_in_graph (xf,is,it)
 
-let cache_coercion o =
-  load_coercion 1 o
+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 subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) =
   let coe' = subst_coe_typ subst coe in
@@ -380,6 +400,7 @@ 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;