diff --git a/tests/notation.v b/tests/notation.v index d1ded9f628942ecd1a21b6b241963547653748a9..bf6093a502266f519baa725f73ee7b86e9e363cf 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 ∧