adapt to coq/coq#19372

imdea-software · Jul 17, 2024 · 6bb3e1c · 6bb3e1c
1 parent 6f46230
commit 6bb3e1c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/core/pred.v b/core/pred.v
@@ -1178,7 +1178,7 @@ Definition id_rel : Rel A := fun x y => y = x.
 Lemma id_rel_refl : forall x, id_rel x x.
 Proof. by []. Qed.
 Lemma id_rel_sym : Symmetric id_rel.
-Proof. by []. Qed.
+Proof. by move=> *; split. Qed.
 Lemma id_rel_trans : Transitive id_rel.
 Proof. by move=> x y z ->->. Qed.
 Lemma id_rel_func : functional id_rel.