diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-04-19 12:07:44 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-04-19 12:09:24 -0400 |
| commit | a75a26ca7f6c66b0d85f79315b9f8d7550cd5066 (patch) | |
| tree | 06985149c98be9c6561772436da9dfea9a96c929 /_CoqProject | |
| parent | ccd934fbd94229469a8da90b52be16545d31e191 (diff) | |
Add a tactic for field inequalities
Pair programming with Andres, a better proof of unifiedAddM1'_rep, some
progress on twistedAddAssoc.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 3 |
1 files changed, 2 insertions, 1 deletions
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 |