diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-02 11:08:32 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-03 15:08:18 -0400 |
| commit | d969b7e3c0ffcf997887e099d0917ac3a31ae5aa (patch) | |
| tree | 51df72743df8e1d3938c620c3c5c408a8c6fbb13 /_CoqProject | |
| parent | c823881fa6b528135a08e55b85713e107c6ada58 (diff) | |
Remove old reflective pipeline, making way the new
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/_CoqProject b/_CoqProject index 83600e507..20a560af2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -201,9 +201,6 @@ src/Reflection/Z/HexNotationConstants.v src/Reflection/Z/Inline.v src/Reflection/Z/InlineInterp.v src/Reflection/Z/InlineWf.v -src/Reflection/Z/Interpretations128.v -src/Reflection/Z/Interpretations64.v -src/Reflection/Z/InterpretationsGen.v src/Reflection/Z/JavaNotations.v src/Reflection/Z/MapCastByDeBruijn.v src/Reflection/Z/MapCastByDeBruijnInterp.v @@ -214,10 +211,6 @@ src/Reflection/Z/Syntax.v src/Reflection/Z/Bounds/Interpretation.v src/Reflection/Z/Bounds/MapCastByDeBruijn.v src/Reflection/Z/Bounds/Relax.v -src/Reflection/Z/Interpretations128/Relations.v -src/Reflection/Z/Interpretations128/RelationsCombinations.v -src/Reflection/Z/Interpretations64/Relations.v -src/Reflection/Z/Interpretations64/RelationsCombinations.v src/Reflection/Z/Syntax/Equality.v src/Reflection/Z/Syntax/Util.v src/Spec/CompleteEdwardsCurve.v @@ -231,40 +224,12 @@ src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v -src/Specific/GF25519BoundedCommon.v src/Specific/IntegrationTest.v src/Specific/NewBaseSystemTest.v src/Specific/SC25519.v src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v -src/Specific/GF25519Reflective/Common.v -src/Specific/GF25519Reflective/Common9_4Op.v -src/Specific/GF25519Reflective/CommonBinOp.v -src/Specific/GF25519Reflective/CommonUnOp.v -src/Specific/GF25519Reflective/CommonUnOpFEToWire.v -src/Specific/GF25519Reflective/CommonUnOpFEToZ.v -src/Specific/GF25519Reflective/CommonUnOpWireToFE.v -src/Specific/GF25519Reflective/Reified.v -src/Specific/GF25519Reflective/Reified/Add.v -src/Specific/GF25519Reflective/Reified/AddCoordinates.v -src/Specific/GF25519Reflective/Reified/AddDisplay.v -src/Specific/GF25519Reflective/Reified/AddJavaDisplay.v -src/Specific/GF25519Reflective/Reified/CarryAdd.v -src/Specific/GF25519Reflective/Reified/CarryOpp.v -src/Specific/GF25519Reflective/Reified/CarrySub.v -src/Specific/GF25519Reflective/Reified/GeModulus.v -src/Specific/GF25519Reflective/Reified/LadderStep.v -src/Specific/GF25519Reflective/Reified/LadderStepDisplay.v -src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v -src/Specific/GF25519Reflective/Reified/Mul.v -src/Specific/GF25519Reflective/Reified/MulDisplay.v -src/Specific/GF25519Reflective/Reified/MulJavaDisplay.v -src/Specific/GF25519Reflective/Reified/Opp.v -src/Specific/GF25519Reflective/Reified/Pack.v -src/Specific/GF25519Reflective/Reified/PreFreeze.v -src/Specific/GF25519Reflective/Reified/Sub.v -src/Specific/GF25519Reflective/Reified/Unpack.v src/Tactics/VerdiTactics.v src/Tactics/Algebra_syntax/Nsatz.v src/Test/Curve25519SpecTestVectors.v |