Merge PR #8920: Deprecate Typeclasses Axioms Are Instances

5 files changed, 10 insertions, 1 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 6bdb63d4d7..5ff90b5123 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -120,6 +120,10 @@ Universes
 - Added `Print Universes Subgraph` variant of `Print Universes`.
   Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).`
 
+Misc
+
+- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index dc1397aff2..5e031efa85 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.7 *)
+Local Set Warnings "-deprecated".
+
 Require Export Coq.Compat.Coq88.
 
 (* In 8.7, omega wasn't taking advantage of local abbreviations,
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 0aab64e4c4..989072940a 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+Local Set Warnings "-deprecated".
+
 Require Export Coq.Compat.Coq89.
 
 (** In Coq 8.9, prim token notations follow [Import] rather than
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index d25671887f..49b9e4c951 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -9,3 +9,4 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.9 *)
+Local Set Warnings "-deprecated".
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 8707121306..ef28fc2d77 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -29,7 +29,7 @@ let axiom_into_instance = ref false
 let _ =
   let open Goptions in
   declare_bool_option
-    { optdepr = false;
+    { optdepr = true;
       optname = "automatically declare axioms whose type is a typeclass as instances";
       optkey = ["Typeclasses";"Axioms";"Are";"Instances"];
       optread = (fun _ -> !axiom_into_instance);