From 57c98ce1ff8bf572ec93e237c93caea6cb22a12c Mon Sep 17 00:00:00 2001
From: Alix Trieu <alix.trieu@cs.au.dk>
Date: Mon, 22 Mar 2021 13:50:19 +0100
Subject: [PATCH] Apply Robbert's suggestions

---
 theories/finite.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/theories/finite.v b/theories/finite.v
index 4297363d..9e58dcd6 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -224,11 +224,12 @@ Section surjective_finite.
   Context `{Finite A, EqDecision B} (f : A → B).
   Context `{!Surj (=) f}.
 
-  Program Instance surjective_finite: Finite B := {| enum := remove_dups (f <$> enum A) |}.
+  Program Instance surjective_finite: Finite B :=
+    {| enum := remove_dups (f <$> enum A) |}.
   Next Obligation. apply NoDup_remove_dups. Qed.
   Next Obligation.
     intros y. rewrite elem_of_remove_dups, elem_of_list_fmap.
-    destruct (Surj0 y). eauto using elem_of_enum.
+    destruct (surj f y). eauto using elem_of_enum.
   Qed.
 End surjective_finite.
 
@@ -236,9 +237,9 @@ Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Program Instance bijective_finite: Finite B := _.
-  Next Obligation. eapply surjective_finite. eapply cancel_surj.
-                   Unshelve. all: eapply _. Qed.
+  Global Instance bijective_finite: Finite B :=
+    let _ := cancel_surj (f:=f) (g:=g) in
+    surjective_finite f.
 End bijective_finite.
 
 Program Instance option_finite `{Finite A} : Finite (option A) :=
-- 
GitLab