aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Make
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Make')
-rw-r--r--coqprime/Make52
1 files changed, 52 insertions, 0 deletions
diff --git a/coqprime/Make b/coqprime/Make
new file mode 100644
index 000000000..efedc2a37
--- /dev/null
+++ b/coqprime/Make
@@ -0,0 +1,52 @@
+-R Tactic Coqprime
+-R N Coqprime
+-R List Coqprime
+-R Z Coqprime
+-R PrimalityTest Coqprime
+-R elliptic Coqprime
+-R num Coqprime
+-R examples Coqprime
+
+Tactic/Tactic.v
+N/NatAux.v
+List/Iterator.v
+List/ListAux.v
+List/Permutation.v
+List/UList.v
+List/ZProgression.v
+Z/Pmod.v
+Z/ZCAux.v
+Z/Zmod.v
+Z/Ppow.v
+Z/ZCmisc.v
+Z/ZSum.v
+PrimalityTest/Cyclic.v
+PrimalityTest/EGroup.v
+PrimalityTest/Euler.v
+PrimalityTest/FGroup.v
+PrimalityTest/IGroup.v
+PrimalityTest/Lagrange.v
+PrimalityTest/LucasLehmer.v
+PrimalityTest/Pepin.v
+PrimalityTest/PGroup.v
+PrimalityTest/PocklingtonCertificat.v
+PrimalityTest/Pocklington.v
+PrimalityTest/Proth.v
+PrimalityTest/Root.v
+PrimalityTest/Zp.v
+elliptic/GZnZ.v
+elliptic/SMain.v
+elliptic/ZEll.v
+num/Bits.v
+num/Lucas.v
+num/NEll.v
+num/MEll.v
+num/Mod_op.v
+num/Pock.v
+num/montgomery.v
+num/W.v
+examples/BasePrimes.v
+examples/PocklingtonRefl.v
+
+
+