diff --git a/tests/solve_proper.v b/tests/solve_proper.v
index 1f44e13d742222f0d06cc8c5b441163592d5222e..d4e4d665e7c1cadd9fc52ac7892b785c21c9e8a7 100644
--- a/tests/solve_proper.v
+++ b/tests/solve_proper.v
@@ -9,16 +9,16 @@ Section tests.
             !Proper ((≡) ==> (≡) ==> (≡)) baz}.
 
   Definition test1 (x : A) := baz (bar (foo x)) x.
-  Global Instance : Proper ((≡) ==> (≡)) test1.
+  Goal Proper ((≡) ==> (≡)) test1.
   Proof. solve_proper. Qed.
 
   Definition test2 (b : bool) (x : A) :=
     if b then bar (foo x) else bar x.
-  Global Instance : ∀ b, Proper ((≡) ==> (≡)) (test2 b).
+  Goal ∀ b, Proper ((≡) ==> (≡)) (test2 b).
   Proof. solve_proper. Qed.
 
   Definition test3 (f : nat → A) :=
     baz (bar (f 0)) (f 2).
-  Global Instance : Proper (pointwise_relation nat (≡) ==> (≡)) test3.
+  Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3.
   Proof. solve_proper. Qed.
 End tests.