From a232a1f68207bb8a5c2a1a5740b888a35564151d Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Wed, 31 Jan 2024 10:43:53 +0100 Subject: [PATCH] Globla :: instance --- 3rdparty/ALEA/Ccpo.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/3rdparty/ALEA/Ccpo.v b/3rdparty/ALEA/Ccpo.v index 856956d..621abb9 100644 --- a/3rdparty/ALEA/Ccpo.v +++ b/3rdparty/ALEA/Ccpo.v @@ -52,7 +52,7 @@ Opaque OrderEquiv. Class ord A := { Oeq : relation A; Ole : relation A; - order_rel : Order Oeq Ole }. + #[global] order_rel :: Order Oeq Ole }. Lemma OrdSetoid `(o:ord A) : Setoid A.