aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/field/Make
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/field/Make')
-rw-r--r--mathcomp/field/Make14
1 files changed, 14 insertions, 0 deletions
diff --git a/mathcomp/field/Make b/mathcomp/field/Make
new file mode 100644
index 0000000..93ff57c
--- /dev/null
+++ b/mathcomp/field/Make
@@ -0,0 +1,14 @@
+all.v
+algC.v
+algebraics_fundamentals.v
+algnum.v
+closed_field.v
+countalg.v
+cyclotomic.v
+falgebra.v
+fieldext.v
+finfield.v
+galois.v
+separable.v
+
+-R . mathcomp.field