diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-28 16:33:06 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-28 16:56:17 -0500 |
| commit | 761259c947ebe2ba94c71b5121b6790bc6d9d1e6 (patch) | |
| tree | 1384d750705dd10a08300a8592d918d518d68c2e /_CoqProject | |
| parent | 63af66f190350b1fdfe9f905eb88d996a23f68a9 (diff) | |
ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoordinates, outline Edwards curve associativity
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index c1a88976f..3adab537f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,6 +7,7 @@ src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v +src/ModularArithmetic/FField.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/Pre.v |