aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-05-06 22:17:10 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-06-17 13:00:26 -0400
commit037df57566b1108af0d13cfcafe9b0f8fdd5937b (patch)
tree9310260156d8d1e19215fb4765b5a4e64dc9a9d2 /src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v
parenta073821cf7ba0714a30e892af40bd309cd5f2f03 (diff)
New pipeline, split among files
Diffstat (limited to 'src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v')
-rw-r--r--src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v b/src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v
new file mode 100644
index 000000000..225649b99
--- /dev/null
+++ b/src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Experiments.NewPipeline.StandaloneHaskellMain.
+
+(*Redirect "/tmp/unsaturated_solinas.hs" *)Recursive Extraction UnsaturatedSolinas.main.
+(* cat /tmp/solinas.hs.out | sed -f haskell.sed > ../../solinas.hs *)