From 370c0cf4d1cb4eb34c10d90d972eeed238905afb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Jun 2020 11:13:32 +0200
Subject: [PATCH] Fix compatibility with old Coq versions.
---
theories/finite.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/finite.v b/theories/finite.v
index f5d516cc..d24e9c1e 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -154,7 +154,7 @@ Lemma finite_bijective A `{Finite A} B `{Finite B} :
Proof.
split.
- intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
- exists f; eauto using finite_inj_surj.
+ exists f; split; [done|]. by apply finite_inj_surj.
- intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ by exists f.
+ destruct (surj_cancel f) as (g&?). exists g. apply cancel_inj.
@@ -274,7 +274,7 @@ Next Obligation.
Qed.
Next Obligation.
intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
- eauto using elem_of_enum.
+ [left|right]; (eexists; split; [done|apply elem_of_enum]).
Qed.
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
--
GitLab