From 1ea69cd53ff8472bb23c338d0e3fcac0a1f9ada5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 16 Sep 2016 13:31:40 -0400 Subject: Derive EdDSA.verify from equational specification Experiments/SpecEd25519 will come back soon --- _CoqProject | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to '_CoqProject') 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 -- cgit v1.2.3