From 0ad26633a4589d77de1f864733d1d953dab9ea91 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 19 Nov 2017 22:53:28 +0100
Subject: Fix (partial) #4878: option to stop autodeclaring axiom as instance.

---
 test-suite/success/Typeclasses.v | 17 +++++++++++++++++
 test-suite/success/bteauto.v     |  1 +
 2 files changed, 18 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 6b1f0315bc..cd6eac35cf 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 3178c6fc15..730b367d60 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.
     
-- 
cgit v1.2.3