Merge PR #8094: Remove `Automatic Coercions Import` option.

Reviewed-by: ppedrot

5 files changed, 7 insertions, 55 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 4a66fa423e..764d4afb5c 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -149,6 +149,8 @@ Vernacular commands
 
 - `Hypotheses` and `Variables` can now take implicit binders inside sections.
 
+- Removed deprecated option `Automatic Coercions Import`.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index d15aacad44..795fccbf08 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -322,21 +322,8 @@ are also forgotten.
 Coercions and Modules
 ---------------------
 
-.. flag:: Automatic Coercions Import
-
-   Since |Coq| version 8.3, the coercions present in a module are activated
-   only when the module is explicitly imported. Formerly, the coercions
-   were activated as soon as the module was required, whether it was
-   imported or not.
-
-   This option makes it possible to recover the behavior of the versions of
-   |Coq| prior to 8.3.
-
-.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
-
-   This warning is emitted when typechecking relies on a coercion
-   contained in a module that has not been explicitely imported. It helps
-   migrating code and stop relying on the option above.
+The coercions present in a module are activated only when the module is
+explicitly imported.
 
 Examples
 --------
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 54a1aa9aa0..ef918a614e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -120,9 +120,6 @@ let class_tab =
 let coercion_tab =
   Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
-let coercions_in_scope =
-  Summary.ref ~name:"coercions_in_scope" GlobRef.Set_env.empty
-
 module ClPairOrd =
 struct
   type t = cl_index * cl_index
@@ -400,13 +397,6 @@ let class_params = function
 let add_class cl =
   add_new_class cl { cl_param = class_params cl }
 
-let get_automatically_import_coercions =
-  Goptions.declare_bool_option_and_ref
-    ~depr:true (* Remove in 8.8 *)
-    ~name:"automatic import of coercions"
-    ~key:["Automatic";"Coercions";"Import"]
-    ~value:false
-
 let cache_coercion (_, c) =
   let () = add_class c.coercion_source in
   let () = add_class c.coercion_target in
@@ -422,20 +412,9 @@ let cache_coercion (_, c) =
   let () = add_new_coercion c.coercion_type xf in
   add_coercion_in_graph (xf,is,it)
 
-let load_coercion _ o =
-  if get_automatically_import_coercions () then
-    cache_coercion o
-
-let set_coercion_in_scope (_, c) =
-  let r = c.coercion_type in
-  coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope
-
 let open_coercion i o =
-  if Int.equal i 1 then begin
-    set_coercion_in_scope o;
-    if not (get_automatically_import_coercions ()) then
-      cache_coercion o
-  end
+  if Int.equal i 1 then
+    cache_coercion o
 
 let subst_coercion (subst, c) =
   let coe = subst_coe_typ subst c.coercion_type in
@@ -469,10 +448,7 @@ let classify_coercion obj =
 let inCoercion : coercion -> obj =
   declare_object {(default_object "COERCION") with
     open_function = open_coercion;
-    load_function = load_coercion;
-    cache_function = (fun objn ->
-        set_coercion_in_scope objn;
-        cache_coercion objn);
+    cache_function = cache_coercion;
     subst_function = subst_coercion;
     classify_function = classify_coercion;
     discharge_function = discharge_coercion }
@@ -532,6 +508,3 @@ let hide_coercion coe =
     let coe_info = coercion_info coe in
     Some coe_info.coe_param
   else None
-
-let is_coercion_in_scope r =
-  GlobRef.Set_env.mem r !coercions_in_scope
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 7c4842c8ae..ed2c5478f0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -113,5 +113,3 @@ val coercions : unit -> coe_info_typ list
 (** [hide_coercion] returns the number of params to skip if the coercion must
    be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
 val hide_coercion : coe_typ -> int option
-
-val is_coercion_in_scope : GlobRef.t -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 82411ba2ef..8c9b6550f3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -368,20 +368,12 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
-let warn_coercion_not_in_scope =
-  CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated"
-    Pp.(fun r -> str "Coercion used but not in scope: " ++
-              Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use "
-              ++ str "this coercion, please Import the module that contains it.")
-
 (* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
       List.fold_left
         (fun (ja,typ_cl,sigma) i ->
-           if not (is_coercion_in_scope i.coe_value) then
-             warn_coercion_not_in_scope i.coe_value;
            let isid = i.coe_is_identity in
            let isproj = i.coe_is_projection in
            let sigma, c = new_global sigma i.coe_value in