From a75a26ca7f6c66b0d85f79315b9f8d7550cd5066 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Apr 2016 12:07:44 -0400 Subject: Add a tactic for field inequalities Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc. --- _CoqProject | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 1d65a7564..ea5503260 100644 --- a/_CoqProject +++ b/_CoqProject @@ -16,8 +16,8 @@ src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemProofs.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v -src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v @@ -34,5 +34,6 @@ src/Util/IterAssocOp.v src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v +src/Util/Tactics.v src/Util/WordUtil.v src/Util/ZUtil.v -- cgit v1.2.3