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