From ebfdbffdac6b0aff4f161b5eebb6f89c4b71edc1 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 28 Apr 2026 16:27:16 +0200 Subject: [PATCH] Adapt to math-comp/math-comp#1580 --- pcm/minus.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pcm/minus.v b/pcm/minus.v index 5f3f528..0605162 100644 --- a/pcm/minus.v +++ b/pcm/minus.v @@ -488,8 +488,8 @@ HB.instance Definition _ := TPCMS.on oint2. Module RWsep. Import intZmod intOrdered ssralg.GRing ssralg.GRing.Theory Num.Theory Num.Def. -Import order.Order.TTheory order.Order.DefaultProdOrder order.Order.ProdSyntax. -Import order.Order.DefaultProdLexiOrder order.Order.LexiSyntax. +Import Order.TTheory Order.DefaultProdOrder Order.ProdSyntax. +Import Order.DefaultProdLexiOrder Order.LexiSyntax. Local Open Scope order_scope. Local Open Scope ring_scope.