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.

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index c770382da..d5305641e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-COQ_ARGS := -R bedrock/Bedrock Bedrock
+COQ_ARGS := -R bedrock/Bedrock Bedrock -R coqprime/Tactic Coqprime -R coqprime/N Coqprime -R coqprime/Z Coqprime -R coqprime/List Coqprime -R coqprime/PrimalityTest Coqprime
 MOD_NAME := Crypto
 SRC_DIR  := src
 MODULES  := Curves Galois Rep Specific Tactics Util
-- 
cgit v1.2.3