From c63e367832b56d29255e11c390f185dc93b36bcf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 28 Jan 2021 18:32:28 +0100
Subject: [PATCH] Do not declare tests as Instances.

---
 tests/solve_proper.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/solve_proper.v b/tests/solve_proper.v
index 1f44e13d..d4e4d665 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.
-- 
GitLab