6 files changed, 24 insertions, 24 deletions
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 9086621344..3888cafed3 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -14,7 +14,7 @@ Module onlyclasses.
   Module RJung.
     Class Foo (x : nat).
       
-      Instance foo x : x = 2 -> Foo x.
+      Instance foo x : x = 2 -> Foo x := {}.
       Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
       Typeclasses eauto := debug.
       Check (_ : Foo 2).
@@ -63,7 +63,7 @@ End RefineVsNoTceauto.
 Module Leivantex2PR339.
   (** Was a bug preventing to find hints associated with no pattern *)
   Class Bar := {}.
-  Instance bar1 (t:Type) : Bar.
+  Instance bar1 (t:Type) : Bar := {}.
   Hint Extern 0 => exact True : typeclass_instances.
   Typeclasses eauto := debug.
   Goal Bar.
@@ -222,10 +222,10 @@ Module IterativeDeepening.
   Class B.
   Class C.
 
-  Instance: B -> A | 0.
-  Instance: C -> A | 0.
-  Instance: C -> B -> A | 0.
-  Instance: A -> A | 0.
+  Instance: B -> A | 0 := {}.
+  Instance: C -> A | 0 := {}.
+  Instance: C -> B -> A | 0 := {}.
+  Instance: A -> A | 0 := {}.
   
   Goal C -> A.
     intros.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index 5477c83316..62a66daf7d 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -51,7 +51,7 @@ Qed.
 
 Class B (A : Type).
 Class I. 
-Instance i : I.
+Instance i : I := {}.
   
 Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
 Class D (f : nat -> nat -> nat).
@@ -59,7 +59,7 @@ Definition ftest (x y : nat) := x + y.
 Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
   Admitted.
 Module Instnopat.
-  Local Instance: B nat.
+  Local Instance: B nat := {}.
   (* pattern_of_constr -> B nat *)
   (* exact hint *)
   Check (_ : B nat).
@@ -72,7 +72,7 @@ Module Instnopat.
     eauto with typeclass_instances.
   Qed.
 
-  Local Instance: D ftest.
+  Local Instance: D ftest := {}.
   Local Hint Resolve flipD | 0 : typeclass_instances.
   (* pattern: D (flip _) *)
   Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)  
@@ -80,7 +80,7 @@ Module Instnopat.
 End Instnopat.
 
 Module InstnopatApply.
-  Local Instance: I -> B nat.
+  Local Instance: I -> B nat := {}.
   (* pattern_of_constr -> B nat *)
   (* apply hint  *)
   Check (_ : B nat).
@@ -116,7 +116,7 @@ Module InstPat.
 
   Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
   Module withftest.
-    Local Instance: D ftest.
+    Local Instance: D ftest := {}.
 
     Check (_ : D _).
     (* D_instance_0 : D ftest *)
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 730b367d60..cea7d92c0b 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -149,10 +149,10 @@ Module IterativeDeepening.
   Class B.
   Class C.
 
-  Instance: B -> A | 0.
-  Instance: C -> A | 0.
-  Instance: C -> B -> A | 0.
-  Instance: A -> A | 0.
+  Instance: B -> A | 0 := {}.
+  Instance: C -> A | 0 := {}.
+  Instance: C -> B -> A | 0 := {}.
+  Instance: A -> A | 0 := {}.
   
   Goal C -> A.
     intros.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index d1d384659b..573912c7cd 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -263,7 +263,7 @@ Abort.
 (* This one was working in 8.4 (because of full conv on closed arguments) *)
 
 Class E.
-Instance a:E.
+Instance a:E := {}.
 Goal forall h : E -> nat -> nat, h (id a) 0 = h a 0.
 intros.
 destruct (h _).
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index c44747379f..5b616ccc33 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -9,11 +9,11 @@
 (************************************************************************)
 
 Class A (A : Type).
-  Instance an: A nat.
+  Instance an: A nat := {}.
 
 Class B (A : Type) (a : A).
-Instance bn0: B nat 0.
-Instance bn1: B nat 1.
+Instance bn0: B nat 0 := {}.
+Instance bn1: B nat 1 := {}.
 
 Goal A nat.
 Proof.
@@ -39,7 +39,7 @@ Proof.
   eexists. eexists. typeclasses eauto.
 Defined.
 
-Instance ab: A bool. (* Backtrack on A instance *)
+Instance ab: A bool := {}. (* Backtrack on A instance *)
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
   eexists. eexists. typeclasses eauto.
@@ -51,7 +51,7 @@ Hint Extern 0 { x : ?A & _ } =>
   unshelve class_apply @existT : typeclass_instances.
 Existing Class sigT.
 Set Typeclasses Debug.
-Instance can: C an 0.
+Instance can: C an 0 := {}.
 (* Backtrack on instance implementation *)
 Goal exists (T : Type) (t : T), { x : A T & C x t }.
 Proof.
@@ -59,7 +59,7 @@ Proof.
 Defined.
 
 Class D T `(a: A T).
-  Instance: D _ an.
+  Instance: D _ an := {}.
 Goal exists (T : Type), { x : A T & D T x }.
 Proof.
   eexists. typeclasses eauto.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index 79467e549c..351481b0b6 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop.
 Axiom SetoidS1 : Setoid_Theory S1 eqS1.
 Add Setoid S1 eqS1 SetoidS1 as S1setoid.
 
-Instance eqS1_default : DefaultRelation eqS1.
+Instance eqS1_default : DefaultRelation eqS1 := {}.
 
 Axiom eqS1': S1 -> S1 -> Prop.
 Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
@@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
 Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
 Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
 
-Instance eqS1_test8_default : DefaultRelation eqS1_test8.
+Instance eqS1_test8_default : DefaultRelation eqS1_test8 := {}.
 
 Axiom f_test8 : S2 -> S1_test8.
 Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted.