diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-16 13:31:40 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-16 19:00:06 -0400 |
| commit | 1ea69cd53ff8472bb23c338d0e3fcac0a1f9ada5 (patch) | |
| tree | 14379b1df13a789daf454f29324661ebb85c9f0c /_CoqProject | |
| parent | 7d139ded819549c587b169e6ef54d411bc543cd4 (diff) | |
Derive EdDSA.verify from equational specification
Experiments/SpecEd25519 will come back soon
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/_CoqProject b/_CoqProject index d87842e49..797f2a12c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -38,8 +38,6 @@ src/Encoding/PointEncodingPre.v src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v -src/Experiments/SpecEd25519.v -src/Experiments/SpecificCurve25519.v src/ModularArithmetic/ExtPow2BaseMulProofs.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v @@ -102,12 +100,14 @@ src/Util/HProp.v src/Util/Isomorphism.v src/Util/IterAssocOp.v src/Util/ListUtil.v +src/Util/Logic.v src/Util/NatUtil.v src/Util/Notations.v src/Util/NumTheoryUtil.v src/Util/Option.v src/Util/PointedProp.v src/Util/Prod.v +src/Util/Relations.v src/Util/Sigma.v src/Util/Sum.v src/Util/Tactics.v |