aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/field/Make
diff options
context:
space:
mode:
authorCyril Cohen2018-07-28 21:30:02 +0200
committerCyril Cohen2018-10-26 03:33:07 +0200
commitbccc54dc85e2d9cd7248c24a576d6092630fb51d (patch)
treedeb09d0b341008596781f2ceafa69bc84fc5b86f /mathcomp/field/Make
parent76fb3c00580488f75362153f6ea252f9b4d4084b (diff)
moving countalg and closed_field around
- countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style
Diffstat (limited to 'mathcomp/field/Make')
-rw-r--r--mathcomp/field/Make1
1 files changed, 0 insertions, 1 deletions
diff --git a/mathcomp/field/Make b/mathcomp/field/Make
index 00aa7a5..b7c3f13 100644
--- a/mathcomp/field/Make
+++ b/mathcomp/field/Make
@@ -3,7 +3,6 @@ algC.v
algebraics_fundamentals.v
algnum.v
closed_field.v
-countalg.v
cyclotomic.v
falgebra.v
fieldext.v