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

12 files changed, 35 insertions, 35 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.
 
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.