Merge pull request #42 from gares/done

adapt to coq/coq#19372
imdea-software · Jul 17, 2024 · e29ad1f · e29ad1f
2 parents 6f46230 + 6bb3e1c
commit e29ad1f
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.