From 8b3728b68ea21e0cfedfc4eff7fa15830e84bdf1 Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@mit.edu>
Date: Wed, 20 Jan 2016 15:54:08 -0500
Subject: Import coqprime; use it to prove Euler's criterion.

---
 coqprime/Make | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 coqprime/Make

(limited to 'coqprime/Make')

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
+
+
+
-- 
cgit v1.2.3