From 6bb3e1c7764947d12d45106c6b151cdf88e21797 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Jul 2024 10:51:31 +0200 Subject: [PATCH] adapt to coq/coq#19372 --- core/pred.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/pred.v b/core/pred.v index 256d6c3..d7b9a1e 100644 --- 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.