diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 03:50:08 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 03:50:08 -0400 |
| commit | 3febea4ed8fdb255c634acbeb3705c88baa89303 (patch) | |
| tree | 94988bf2c544dcdab18131761bb9a5b08c20fcad /_CoqProject | |
| parent | aafcec91728330c79d74f4c984729cf3aadc3605 (diff) | |
Remove anything incompatible with new algebraic hierarcy
- PointEncoding (these will hopefully come back soon)
- EdDSAProofs (not a priority to bring back, but not hard either)
- Ed25519 spec bits and pieces which were not finished anyway
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/_CoqProject b/_CoqProject index ffb532390..a3458ed1e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,21 +5,18 @@ 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 src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v -src/Encoding/PointEncodingPre.v -src/Encoding/PointEncodingTheorems.v +src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v +src/Experiments/GenericFieldPow.v +src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v @@ -32,12 +29,10 @@ src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v -src/Spec/Ed25519.v src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v -src/Spec/PointEncoding.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v |