Fix (partial) #4878: option to stop autodeclaring axiom as instance.

7 files changed, 51 insertions, 2 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 22c75b4fc..cab673999 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -462,11 +462,18 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}.
 
 This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
 
+\subsection{\tt Set Typeclasses Axioms Are Instances}
+\optindex{Typeclasses Axioms Are Instances}
+
+This option (off by default since 8.8) automatically declares axioms
+whose type is a typeclass at declaration time as instances of that
+class.
+
 \subsection{\tt Set Typeclasses Dependency Order}
 \optindex{Typeclasses Dependency Order}
 
 This option (on by default since 8.6) respects the dependency order between
-subgoals, meaning that subgoals which are depended on by other subgoals 
+subgoals, meaning that subgoals which are depended on by other subgoals
 come first, while the non-dependent subgoals were put before the
 dependent ones previously (Coq v8.5 and below). This can result in quite
 different performance behaviors of proof search.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index da12b6868..5210b2703 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -65,6 +65,7 @@ Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A
 = B.
 Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
 Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V.
+Existing Instance is0trunc_V.
 Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.
 Axiom bisimulation_refl : forall (v : V), bisimulation v v.
 Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index b4c745375..d02a5f120 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C)
 
 Generalizable All Variables.
 Axiom fs : Funext.
+Existing Instance fs.
 
 Section bar.
 
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 6b1f0315b..cd6eac35c 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -240,3 +240,20 @@ Module IterativeDeepening.
   Qed.
 
 End IterativeDeepening.
+
+Module AxiomsAreInstances.
+  Set Typeclasses Axioms Are Instances.
+  Class TestClass1 := {}.
+  Axiom testax1 : TestClass1.
+  Definition testdef1 : TestClass1 := _.
+
+  Unset Typeclasses Axioms Are Instances.
+  Class TestClass2 := {}.
+  Axiom testax2 : TestClass2.
+  Fail Definition testdef2 : TestClass2 := _.
+
+  (* we didn't break typeclasses *)
+  Existing Instance testax2.
+  Definition testdef2 : TestClass2 := _.
+
+End AxiomsAreInstances.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 3178c6fc1..730b367d6 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -55,6 +55,7 @@ Module Backtracking.
     Axiom A : Type.
     Existing Class A.
     Axioms a b c d e: A.
+    Existing Instances a b c d e.
     
     Ltac get_value H := eval cbv delta [H] in H.
     
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index ef1737bf8..aeef9595d 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -15,3 +15,6 @@
    and breaks at least fiat-crypto. *)
 Declare ML Module "omega_plugin".
 Unset Omega UseLocalDefs.
+
+
+Set Typeclasses Axioms Are Instances.
diff --git a/vernac/command.ml b/vernac/command.ml
index 373e5a1be..01c7f149b 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -174,6 +174,24 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
+let axiom_into_instance = ref false
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optdepr = false;
+      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 = function
+  | Discharge ->
+    (* The typeclass behaviour of Variable and Context doesn't depend
+       on section status *)
+    true
+  | Global | Local -> !axiom_into_instance
+
 let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
 match local with
 | Discharge when Lib.sections_are_opened () ->
@@ -195,6 +213,7 @@ match local with
   (r,Univ.Instance.empty,true)
 
 | Global | Local | Discharge ->
+  let do_instance = should_axiom_into_instance local in
   let local = DeclareDef.get_locality ident ~kind:"axiom" local in
   let inl = match nl with
     | NoInline -> None
@@ -207,7 +226,7 @@ match local with
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Universes.register_universe_binders gr pl in
   let () = assumption_message ident in
-  let () = Typeclasses.declare_instance None false gr in
+  let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = match ctx with
     | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx