Turn `Refine Instance Mode` off by default

6 files changed, 15 insertions, 4 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 46de17106d..bcdb951a94 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -98,6 +98,9 @@ Vernacular commands
 
 - `Declare Instance` now requires an instance name.
 
+- Option `Refine Instance Mode` has been turned off by default, meaning that
+  `Instance` no longer opens a proof when a body is provided.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v
index 801c61b132..a321bb324e 100644
--- a/test-suite/bugs/closed/bug_2830.v
+++ b/test-suite/bugs/closed/bug_2830.v
@@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A).
 Admitted.
 
 Import FunctionalExtensionality.
-Instance set_cat : Category Type (fun A B => A -> B) := {
+
+Instance set_cat : Category Type (fun A B => A -> B).
+refine {|
   id := fun A => fun x => x
   ; comp c b a f g := fun x => f (g x)
   ; eqv := fun A B => @skel (A -> B)
-}.
+|}.
 intros. compute. symmetry. apply eta_expansion.
 intros. compute. symmetry. apply eta_expansion.
-intros. compute. reflexivity. Defined.
+intros. compute. reflexivity.
+Defined.
 
 (* The [list] type constructor is a Functor. *)
 
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 78b2aa69b9..9d83743b2a 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -3,7 +3,9 @@ Set Nested Proofs Allowed.
 Class Foo.
 Class Bar := b : Type.
 
+Set Refine Instance Mode.
 Instance foo : Foo := _.
+Unset Refine Instance Mode.
 (* 1 subgoals, subgoal 1 (ID 4)
 
   ============================
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 400479ae85..9086621344 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -198,7 +198,9 @@ Module UniqueInstances.
       for it. *)
   Set Typeclasses Unique Instances.
   Class Eq (A : Type) : Set.
+    Set Refine Instance Mode.
     Instance eqa : Eq nat := _. constructor. Qed.
+    Unset Refine Instance Mode.
     Instance eqb : Eq nat := {}.
     Class Foo (A : Type) (e : Eq A) : Set.
     Instance fooa : Foo _ eqa := {}.
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index 81a087b525..decb5c7519 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -12,3 +12,4 @@
 Local Set Warnings "-deprecated".
 
 Unset Private Polymorphic Universes.
+Set Refine Instance Mode.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6c44745c81..748a2628c5 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration
 open Decl_kinds
 open Entries
 
-let refine_instance = ref true
+let refine_instance = ref false
 
 let () = Goptions.(declare_bool_option {
   optdepr  = false;