From 843e345d5d8217a02de9e7fe20406b83074e807d Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 24 Oct 2019 13:56:19 +0200
Subject: order.v: remove Order.Def, export Order.Syntax by default, and put
 missing scopes

---
 mathcomp/field/algebraics_fundamentals.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index f869378..4fe5f70 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -112,7 +112,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.TTheory Order.Syntax GroupScope GRing.Theory Num.Theory.
+Import Order.TTheory GroupScope GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 Local Notation "p ^ f" := (map_poly f p) : ring_scope.
-- 
cgit v1.2.3