From f566b025ae84efb7e740eb89632988b305c8f1ee Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 26 Feb 2016 15:46:47 -0500 Subject: generic binary exponentiation correctness proof in 3 one-liners --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 61f0fdd3d..c1a88976f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -21,6 +21,7 @@ src/Spec/PointEncoding.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v +src/Util/IterAssocOp.v src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v -- cgit v1.2.3