From 8bd0bdf1631d076b0963f7db061362b6c48737b5 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.