From 2e96e2cab74d00b40188b00a4e90eeeaa1c46706 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 15:08:21 -0400 Subject: EdDSA: prove things about spec --- _CoqProject | 2 ++ 1 file changed, 2 insertions(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index afad38124..904d716b8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -29,6 +29,7 @@ src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v src/Experiments/DerivationsOptionRectLetInEncoding.v +src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v @@ -58,6 +59,7 @@ src/Util/ListUtil.v src/Util/NatUtil.v src/Util/Notations.v src/Util/NumTheoryUtil.v +src/Util/Option.v src/Util/Sum.v src/Util/Tactics.v src/Util/Tuple.v -- cgit v1.2.3