diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 03:13:59 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 03:13:59 -0400 |
| commit | aafcec91728330c79d74f4c984729cf3aadc3605 (patch) | |
| tree | 8699975633a47b5d1929014af1e14eb19ecd1993 /_CoqProject | |
| parent | a7c3e57cb7c3280dfec3a95b18dec83ee6e6d4f4 (diff) | |
| parent | b41ac7998a11354618b122874c03bc68c2833a94 (diff) | |
Merge branch 'field-experiment'
includes broken files to be removed in next commit
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/_CoqProject b/_CoqProject index 4b36c103b..ffb532390 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,11 +2,15 @@ -R Bedrock Bedrock Bedrock/Nomega.v Bedrock/Word.v +src/Algebra.v src/BaseSystem.v src/BaseSystemProofs.v src/EdDSAProofs.v +src/Field.v +src/Nsatz.v src/Rep.v src/Testbit.v +src/UnfinishedDerivations.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -17,8 +21,6 @@ src/Encoding/ModularWordEncodingTheorems.v src/Encoding/PointEncodingPre.v src/Encoding/PointEncodingTheorems.v src/ModularArithmetic/ExtendedBaseVector.v -src/ModularArithmetic/FField.v -src/ModularArithmetic/FNsatz.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemOpt.v @@ -36,7 +38,6 @@ src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v src/Spec/PointEncoding.v -src/Specific/Ed25519.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v @@ -46,5 +47,6 @@ src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v src/Util/Tactics.v +src/Util/Tuple.v src/Util/WordUtil.v src/Util/ZUtil.v |