From 456e29884c4995157a318f176153d4b5f5836959 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 14 Jan 2019 14:50:23 -0500 Subject: separate toplevel2 into several files; fix up final barrett proof --- _CoqProject | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to '_CoqProject') 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 -- cgit v1.2.3