aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-11-05 18:32:57 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2016-11-11 16:07:28 -0500
commit4d6d788ff04ec7b08d522099b6841fd16d6fae5c (patch)
tree9403d8433aa81e4891bef3cc214f07bad820e2ba /_CoqProject
parent188c1cb99886853d452925ae513a44d3da6151dd (diff)
Automatically generate code for field operations with different primes
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject6
1 files changed, 6 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 140b4716a..003c47349 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -164,6 +164,12 @@ src/Specific/GF25519Reflective/Reified/Pack.v
src/Specific/GF25519Reflective/Reified/PreFreeze.v
src/Specific/GF25519Reflective/Reified/Sub.v
src/Specific/GF25519Reflective/Reified/Unpack.v
+src/SpecificGen/GF2213_32.v
+src/SpecificGen/GF2519_32.v
+src/SpecificGen/GF25519_32.v
+src/SpecificGen/GF25519_64.v
+src/SpecificGen/GF41417_32.v
+src/SpecificGen/GF5211_32.v
src/Tactics/VerdiTactics.v
src/Tactics/Algebra_syntax/Nsatz.v
src/Test/Curve25519SpecTestVectors.v