aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-06-17 13:33:17 -0400
committerGravatar Andres Erbsen <andreser@mit.edu>2016-06-17 13:33:17 -0400
commit39ec94341fa3a30d97d4462e9c9d481ada2c8d3d (patch)
treef9c8fddea0a0fae58172c6f012d368df084f0e1d /_CoqProject
parent26640780a5cdce3aed531c1bf7cdaa692244edc7 (diff)
move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 2fc5b1b90..a0fbc5401 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,7 @@ src/BaseSystem.v
src/BaseSystemProofs.v
src/EdDSAProofs.v
src/Field.v
+src/Nsatz.v
src/Rep.v
src/Testbit.v
src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v