Remove deprecated Typeclasses Axioms Are Instances.

5 files changed, 17 insertions, 56 deletions

diff --git a/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst
new file mode 100644
index 0000000000..9fc09c4189
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst
@@ -0,0 +1,3 @@
+- **Removed:** ``Typeclasses Axioms Are Instances`` flag, deprecated since 8.10.
+  Use :cmd:`Declare Instance` for axioms which should be instances
+  (`#11185 <https://github.com/coq/coq/pull/11185>`_, by Théo Zimmermann).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 661aa88082..57a2254100 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -576,14 +576,6 @@ Settings
    of goals.  Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this
    option to 0 turns that flag off.
 
-.. flag:: Typeclasses Axioms Are Instances
-
-   .. deprecated:: 8.10
-
-   This flag (off by default since 8.8) automatically declares axioms
-   whose type is a typeclass at declaration time as instances of that
-   class.
-
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v
index 22fb09526d..d944036112 100644
--- a/test-suite/success/LocalDefinition.v
+++ b/test-suite/success/LocalDefinition.v
@@ -26,28 +26,12 @@ Module TestAdmittedVisibility.
   Fail Check d2.
 End TestAdmittedVisibility.
 
-(* Test consistent behavior of Local Definition wrt automatic declaration of instances *)
-
 Module TestVariableAsInstances.
-  Module Test1.
-    Set Typeclasses Axioms Are Instances.
-    Class U.
-    Local Parameter b : U.
-    Definition testU := _ : U. (* _ resolved *)
-
-    Class T.
-    Variable a : T.  (* warned to be the same as "Local Parameter" *)
-    Definition testT := _ : T. (* _ resolved *)
-  End Test1.
-
-  Module Test2.
-    Unset Typeclasses Axioms Are Instances.
-    Class U.
-    Local Parameter b : U.
-    Fail Definition testU := _ : U. (* _ unresolved *)
+  Class U.
+  Local Parameter b : U.
+  Fail Definition testU := _ : U. (* _ unresolved *)
 
-    Class T.
-    Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
-    Fail Definition testT := _ : T. (* used to succeed *)
-  End Test2.
+  Class T.
+  Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
+  Fail Definition testT := _ : T. (* used to succeed *)
 End TestVariableAsInstances.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 736d05fefc..3f96bf2c35 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -241,13 +241,8 @@ Module IterativeDeepening.
 
 End IterativeDeepening.
 
-Module AxiomsAreInstances.
-  Set Typeclasses Axioms Are Instances.
-  Class TestClass1 := {}.
-  Axiom testax1 : TestClass1.
-  Definition testdef1 : TestClass1 := _.
+Module AxiomsAreNotInstances.
 
-  Unset Typeclasses Axioms Are Instances.
   Class TestClass2 := {}.
   Axiom testax2 : TestClass2.
   Fail Definition testdef2 : TestClass2 := _.
@@ -256,4 +251,4 @@ Module AxiomsAreInstances.
   Existing Instance testax2.
   Definition testdef2 : TestClass2 := _.
 
-End AxiomsAreInstances.
+End AxiomsAreNotInstances.
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e5db6146ca..a001420f74 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -22,24 +22,6 @@ open Entries
 module RelDecl = Context.Rel.Declaration
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-let axiom_into_instance = ref false
-
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr = true;
-      optname = "automatically declare axioms whose type is a typeclass as instances";
-      optkey = ["Typeclasses";"Axioms";"Are";"Instances"];
-      optread = (fun _ -> !axiom_into_instance);
-      optwrite = (:=) axiom_into_instance; }
-
-let should_axiom_into_instance = let open Decls in function
-  | Context ->
-    (* The typeclass behaviour of Variable and Context doesn't depend
-       on section status *)
-    true
-  | Definitional | Logical | Conjectural -> !axiom_into_instance
-
 let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
   let kind = Decls.IsAssumption kind in
   let decl = Declare.SectionLocalAssum {typ; impl} in
@@ -58,7 +40,12 @@ let instance_of_univ_entry = function
   | Monomorphic_entry _ -> Univ.Instance.empty
 
 let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} =
-  let do_instance = should_axiom_into_instance kind in
+  let do_instance = let open Decls in match kind with
+  | Context -> true
+    (* The typeclass behaviour of Variable and Context doesn't depend
+       on section status *)
+  | Definitional | Logical | Conjectural -> false
+  in
   let inl = let open Declaremods in match nl with
     | NoInline -> None
     | DefaultInline -> Some (Flags.get_inline_level())