From f88fe7a60279b782509a6eb00c9c0819ea7ba134 Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Fri, 10 Apr 2020 07:57:02 +0200
Subject: [PATCH] Apply suggestion to tests/notation.v

---
 tests/notation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/notation.v b/tests/notation.v
index d1ded9f6..bf6093a5 100644
--- a/tests/notation.v
+++ b/tests/notation.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base tactics.
 
 (** Test parsing of variants of [(≡)] notation. *)
-Lemma test_equiv_annot_sections `{!Equiv A, Equivalence A (≡@{A})} (x : A) :
+Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
   x ≡@{A} x ∧ (≡@{A}) x x ∧ (x ≡.) x ∧ (.≡ x) x ∧
   ((x ≡@{A} x)) ∧ ((≡@{A})) x x ∧ ((x ≡.)) x ∧ ((.≡ x)) x ∧
   ( x ≡@{A} x) ∧ ( x ≡.) x ∧
-- 
GitLab