diff --git a/modures/cmra.v b/modures/cmra.v index 234f9a1ecc6d8217b0ec32067ab1924f1dbcad81..a9c55a7bcdf9db7d74d0a40fd44c1d2b81d2e684 100644 --- a/modures/cmra.v +++ b/modures/cmra.v @@ -8,7 +8,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ Notation "x ≼{ n } y" := (includedN n x y) (at level 70, format "x ≼{ n } y") : C_scope. Instance: Params (@includedN) 4. -Hint Extern 0 (?x ≼{_} ?x) => reflexivity. +Hint Extern 0 (?x ≼{_} ?y) => reflexivity. Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := { diff --git a/modures/cofe.v b/modures/cofe.v index b508eb45fb94b62ded4c4ee3f41365d81eb08073..5f1e2a4c3ea027bb5db03080cf60854f85237897 100644 --- a/modures/cofe.v +++ b/modures/cofe.v @@ -5,7 +5,7 @@ Class Dist A := dist : nat → relation A. Instance: Params (@dist) 3. Notation "x ={ n }= y" := (dist n x y) (at level 70, n at next level, format "x ={ n }= y"). -Hint Extern 0 (?x ={_}= ?x) => reflexivity. +Hint Extern 0 (?x ={_}= ?y) => reflexivity. Hint Extern 0 (_ ={_}= _) => symmetry; assumption. Tactic Notation "cofe_subst" ident(x) := diff --git a/modures/ra.v b/modures/ra.v index ad6ce17feda9036aee215e8045a8d17f725f4bd9..a6cf97ee036b0416ec614f59641e81cc7349ef23 100644 --- a/modures/ra.v +++ b/modures/ra.v @@ -16,7 +16,7 @@ Notation "(⋅)" := op (only parsing) : C_scope. Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z. Infix "≼" := included (at level 70) : C_scope. Notation "(≼)" := included (only parsing) : C_scope. -Hint Extern 0 (?x ≼ ?x) => reflexivity. +Hint Extern 0 (?x ≼ ?y) => reflexivity. Instance: Params (@included) 3. Class Minus (A : Type) := minus : A → A → A. diff --git a/prelude/base.v b/prelude/base.v index 5ff6bee7b664e8a6994c05bfef095afa943ffc9e..ddbf6334f62fb0822ed76810cbc2ad1b008a8ba3 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -209,9 +209,9 @@ Instance: Params (@equiv) 2. (for types that have an [Equiv] instance) rather than the standard Leibniz equality. *) Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3. -Hint Extern 0 (_ ≡ _) => reflexivity. +Hint Extern 0 (?x ≡ ?y) => reflexivity. Hint Extern 0 (_ ≡ _) => symmetry; assumption. -Hint Extern 0 (_ ≡{_} _) => reflexivity. +Hint Extern 0 (?x ≡{_} ?y) => reflexivity. Hint Extern 0 (_ ≡{_} _) => symmetry; assumption. (** ** Operations on collections *)