diff options
| author |  jadep <jade.philipoom@gmail.com> | 2019-01-14 14:50:23 -0500 |
|---|---|---|
| committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-01-17 09:45:41 +0000 |
| commit | 456e29884c4995157a318f176153d4b5f5836959 (patch) | |
| tree | 67724fbf3a9869db167bc2b8a62e292340169cc4 /_CoqProject | |
| parent | 4441785fb44b88bb6943ddbf639d872c8c903281 (diff) | |
separate toplevel2 into several files; fix up final barrett proof
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index ded3c9adc..ef3ad2d27 100644 --- a/_CoqProject +++ b/_CoqProject @@ -45,7 +45,6 @@ src/RewriterWf2.v src/SlowPrimeSynthesisExamples.v src/StandaloneHaskellMain.v src/StandaloneOCamlMain.v -src/Toplevel2.v src/UnderLets.v src/UnderLetsProofs.v src/Algebra/Field.v @@ -86,6 +85,11 @@ src/ExtractionHaskell/word_by_word_montgomery.v src/ExtractionOCaml/saturated_solinas.v src/ExtractionOCaml/unsaturated_solinas.v src/ExtractionOCaml/word_by_word_montgomery.v +src/Fancy/Barrett256.v +src/Fancy/Montgomery256.v +src/Fancy/Prod.v +src/Fancy/Spec.v +src/Fancy/Translation.v src/Primitives/EdDSARepChange.v src/Primitives/MxDHRepChange.v src/PushButtonSynthesis/ReificationCache.v |