Make `Instance` without a body always open a proof.

6 files changed, 11 insertions, 11 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index 3e3a987a7c..b80e0bb0e4 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn}
 Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}.
 
 Global Instance FunctorApplicationDash C D (F : Functor C D)
-: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0.
+: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}.
 Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B)
-: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100.
+: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}.
 
 Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope.
 
diff --git a/test-suite/bugs/closed/bug_3324.v b/test-suite/bugs/closed/bug_3324.v
index 45dbb57aa2..dae0d4c024 100644
--- a/test-suite/bugs/closed/bug_3324.v
+++ b/test-suite/bugs/closed/bug_3324.v
@@ -6,7 +6,7 @@ Module ETassi.
   Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
   Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
   Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
-  Global Instance isset_hProp : IsHSet hProp | 0.
+  Global Instance isset_hProp : IsHSet hProp | 0 := {}.
 
   Check (eq_refl _ : setT (default_HSet _ _) = hProp).
   Check (eq_refl _ : setT _ = hProp).
@@ -22,7 +22,7 @@ Module JGross.
   Definition Unit_hp:hProp:=(hp Unit admit).
   Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
   Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
-  Global Instance isset_hProp : IsHSet hProp | 0.
+  Global Instance isset_hProp : IsHSet hProp | 0 := {}.
   Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
                                       forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
   Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True.
diff --git a/test-suite/bugs/closed/bug_3454.v b/test-suite/bugs/closed/bug_3454.v
index e4cd60cb24..0a01adec33 100644
--- a/test-suite/bugs/closed/bug_3454.v
+++ b/test-suite/bugs/closed/bug_3454.v
@@ -32,14 +32,14 @@ Local Instance isequiv_tgt_compose A B
 : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
            (A -> B)
            (@compose A {xy : B * B & fst xy = snd xy} B
-                     (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)).
+                     (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)) := {}.
 (* Toplevel input, characters 220-223: *)
 (* Error: Cannot infer this placeholder. *)
 
 Local Instance isequiv_tgt_compose' A B
 : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
            (A -> B)
-           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)).
+           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)) := {}.
 (* Toplevel input, characters 221-232: *)
 (* Error: *)
 (* In environment *)
@@ -52,7 +52,7 @@ Local Instance isequiv_tgt_compose'' A B
 : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
            (A -> B)
            (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _)
-                                                                  (fun s => s.(projT1)))).
+                                                                  (fun s => s.(projT1)))) := {}.
 (* Toplevel input, characters 15-241:
 Error:
 Cannot infer an internal placeholder of type "Type" in environment:
diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v
index 9d37d1a2d0..07b759afb5 100644
--- a/test-suite/bugs/closed/bug_3682.v
+++ b/test-suite/bugs/closed/bug_3682.v
@@ -1,6 +1,6 @@
 Require Import TestSuite.admit.
 Class Foo.
 Definition bar `{Foo} (x : Set) := Set.
-Instance: Foo.
+Instance: Foo := {}.
 Definition bar1 := bar nat.
 Definition bar2 := bar ltac:(admit).
diff --git a/test-suite/bugs/closed/bug_4782.v b/test-suite/bugs/closed/bug_4782.v
index be17a96f15..c08195d502 100644
--- a/test-suite/bugs/closed/bug_4782.v
+++ b/test-suite/bugs/closed/bug_4782.v
@@ -15,8 +15,8 @@ Record T := { dom : Type }.
 Definition pairT A B := {| dom := (dom A * dom B)%type |}.
 Class C (A:Type).
 Parameter B:T.
-Instance c (A:T) : C (dom A).
-Instance cn : C (dom B).
+Instance c (A:T) : C (dom A) := {}.
+Instance cn : C (dom B) := {}.
 Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A.
 Set Typeclasses Debug.
 Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
diff --git a/test-suite/bugs/closed/bug_5401.v b/test-suite/bugs/closed/bug_5401.v
index 95193b993b..466e669d00 100644
--- a/test-suite/bugs/closed/bug_5401.v
+++ b/test-suite/bugs/closed/bug_5401.v
@@ -5,7 +5,7 @@ Parameter P : nat -> Type.
 Parameter v : forall m, P m.
 Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0.
 Class U (R : P 0) (m : forall x, P x) : Prop.
-Instance w : U (f _ (fun _ => v _)) v.
+Instance w : U (f _ (fun _ => v _)) v := {}.
 Print HintDb typeclass_instances.
 End A.