From 8832e45ef9ac8220d220c4f56220d37bc27c2fd4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:28:27 +0100
Subject: Fix doc for Refine Instance Mode

---
 doc/sphinx/addendum/type-classes.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index e77aabfdec..c7ea7e326f 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -559,12 +559,12 @@ Settings
    This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
-   + When it is on (the default), instances that have unsolved holes in
+   + When it is off (the default), they fail with an error instead.
+
+   + When it is on, instances that have unsolved holes in
      their proof-term silently open the proof mode with the remaining
      obligations to prove.
 
-   + When it is off, they fail with an error instead.
-
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3