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.

---
 doc/refman/Classes.tex | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 22c75b4fc8..cab6739998 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.
-- 
cgit v1.2.3