Paolo G. Giarrusso
--- a/tests/notation.v

+ 1

− 1
+++ b/tests/notation.v

+ 1

− 1
 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 ∧