aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/field
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/field')
-rw-r--r--mathcomp/field/algebraics_fundamentals.v2
1 files changed, 1 insertions, 1 deletions
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.