Specify the #[local] hint locality

pi8027 · Jun 7, 2024 · f72c903 · f72c903
1 parent 03bb7e4
commit f72c903
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/misc/usual_stable.v b/misc/usual_stable.v
@@ -12,7 +12,7 @@ Definition eqr {T} (r : rel T) : rel T := [rel x y | r x y && r y x].
 
 Lemma eqr_sym {T} (r : rel T) : symmetric (eqr r).
 Proof. by move=> x y; apply/andP/andP => -[]. Qed.
-Hint Resolve eqr_sym : core.
+#[local] Hint Resolve eqr_sym : core.
 
 Lemma eqrW {T} (r : rel T) : subrel (eqr r) r.
 Proof. by move=> x y /andP[]. Qed.