diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-02-25 13:46:07 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:41:51 -0400 |
| commit | 6a38e9b00458f1dd7d51ec747c73c53a5c258b64 (patch) | |
| tree | 0a99c9d9a6febb7176f77907c403f70cd3331e6c /_CoqProject | |
| parent | eec667b4e9da28b61ac1ac293b6623f12fa61797 (diff) | |
Factor out some bedrock dependencies into WordUtil
Also move a definition about words, with a TODO about location, into WordUtil.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/_CoqProject b/_CoqProject index 333c369b6..61f0fdd3d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,11 +1,11 @@ -R src Crypto src/BaseSystem.v src/BoundedIterOp.v +src/EdDSAProofs.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v -src/EdDSAProofs.v src/Encoding/EncodingTheorems.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v @@ -13,8 +13,9 @@ src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v -src/Spec/EdDSA.v src/Spec/Ed25519.v +src/Spec/EdDSA.v +src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/PointEncoding.v src/Specific/GF25519.v @@ -23,4 +24,5 @@ src/Util/CaseUtil.v src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v +src/Util/WordUtil.v src/Util/ZUtil.v |