From 671dc4c7881517bee661a33cbbbe44dee7273e1a Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Wed, 13 Jul 2016 10:28:01 -0400
Subject: Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s

---
 _CoqProject | 2 ++
 1 file changed, 2 insertions(+)

(limited to '_CoqProject')

diff --git a/_CoqProject b/_CoqProject
index 2ff168ac8..da6abf12b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -33,6 +33,7 @@ src/Experiments/DerivationsOptionRectLetInEncoding.v
 src/Experiments/EdDSARefinement.v
 src/Experiments/GenericFieldPow.v
 src/Experiments/SpecEd25519.v
+src/Experiments/SpecificCurve25519.v
 src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/ModularArithmeticTheorems.v
 src/ModularArithmetic/ModularBaseSystem.v
@@ -57,6 +58,7 @@ src/Specific/GF1305.v
 src/Specific/GF25519.v
 src/Tactics/VerdiTactics.v
 src/Tactics/Algebra_syntax/Nsatz.v
+src/Util/AdditionChainExponentiation.v
 src/Util/CaseUtil.v
 src/Util/Decidable.v
 src/Util/IterAssocOp.v
-- 
cgit v1.2.3