aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra/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/algebra/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/algebra/Make')
-rw-r--r--mathcomp/algebra/Make1
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
index 7d12cb4..b3001f9 100644
--- a/mathcomp/algebra/Make
+++ b/mathcomp/algebra/Make
@@ -1,4 +1,5 @@
all_algebra.v
+countalg.v
finalg.v
fraction.v
intdiv.v