From e4bbfc3ba802d6a8fc1eca47da5202b22b1decaf Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 6 Jul 2016 12:45:20 -0400 Subject: Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util. --- _CoqProject | 2 ++ 1 file changed, 2 insertions(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 904d716b8..55973017b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,6 +37,8 @@ src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v +src/ModularArithmetic/Pow2Base.v +src/ModularArithmetic/Pow2BaseProofs.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v -- cgit v1.2.3