From a7cf802627a9842862c6290496d73a815ab2f42b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Nov 2018 14:41:56 +0100
Subject: Deprecate Typeclasses Axioms Are Instances

People should use Declare Instance instead.
---
 CHANGES.md              | 4 ++++
 vernac/comAssumption.ml | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

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/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);
-- 
cgit v1.2.3


From 47e192dfa40de25a1d1cc51cbd5c6191cdea21b3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Nov 2018 15:20:35 +0100
Subject: Disable deprecation warnings in compat files.

---
 theories/Compat/Coq87.v | 2 ++
 theories/Compat/Coq88.v | 2 ++
 theories/Compat/Coq89.v | 1 +
 3 files changed, 5 insertions(+)

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".
-- 
cgit v1.2.3