From 89ebe23f8e4d362265e3ccc188eedd72c44f55aa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 May 2021 12:03:18 +0200
Subject: [PATCH] =?UTF-8?q?Local=20Instance=20=E2=86=92=20Definition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/finite.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/finite.v b/theories/finite.v
index 60b3961a..c1a0ebc6 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -237,7 +237,7 @@ Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Local Instance bijective_finite: Finite B :=
+  Definition bijective_finite : Finite B :=
     let _ := cancel_surj (f:=f) (g:=g) in
     surjective_finite f.
 End bijective_finite.
-- 
GitLab