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/examples/Make | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 coqprime/examples/Make

(limited to 'coqprime/examples/Make')

diff --git a/coqprime/examples/Make b/coqprime/examples/Make
new file mode 100644
index 000000000..7ad748517
--- /dev/null
+++ b/coqprime/examples/Make
@@ -0,0 +1,18 @@
+-I ../Tactic
+-I ../N
+-I ../Z
+-I ../PrimalityTest
+-I ../List
+-I ../elliptic
+-I ../num
+
+
+BasePrimes.v
+PocklingtonRefl.v
+TestLucas.v
+prime216656403549020227250327256032933021325435259861468456540459488823774358486649614451547405419273433458932168893949521787.v
+prime329719147332060395689499.v  
+russell1.v
+russell2.v
+
+
-- 
cgit v1.2.3