change finfield from field to character

4 files changed, 0 insertions, 3 deletions

diff --git a/mathcomp/field/finfield.v b/mathcomp/character/finfield.v
index 14a02ef..14a02ef 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/character/finfield.v
diff --git a/mathcomp/field/Make b/mathcomp/field/Make
index 93ff57c..6ff83ec 100644
--- a/mathcomp/field/Make
+++ b/mathcomp/field/Make
@@ -7,7 +7,6 @@ countalg.v
 cyclotomic.v
 falgebra.v
 fieldext.v
-finfield.v
 galois.v
 separable.v
 
diff --git a/mathcomp/field/all.v b/mathcomp/field/all.v
index a57ac19..c26dbba 100644
--- a/mathcomp/field/all.v
+++ b/mathcomp/field/all.v
@@ -6,6 +6,5 @@ Require Export countalg.
 Require Export cyclotomic.
 Require Export falgebra.
 Require Export fieldext.
-Require Export finfield.
 Require Export galois.
 Require Export separable.
diff --git a/mathcomp/solvable/all.v b/mathcomp/solvable/all.v
index 72405c5..8c2ea8f 100644
--- a/mathcomp/solvable/all.v
+++ b/mathcomp/solvable/all.v
@@ -16,4 +16,3 @@ Require Export nilpotent.
 Require Export pgroup.
 Require Export primitive_action.
 Require Export sylow.
-Require Export wielandt_fixpoint.