diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 1 |
2 files changed, 5 insertions, 4 deletions
@@ -101,11 +101,11 @@ src/Experiments/X25519.hs: src/Experiments/X25519_noimports.hs src/Experiments/E sed 's/ X25519_noimports / X25519 /g' \ > X25519.hs ) -src/Experiments/Ed25519.o src/Experiments/Ed25519.core: src/Experiments/Ed25519.hs - ( cd src/Experiments && ghc -XStrict -O3 Ed25519.hs -ddump-simpl > Ed25519.core ) +src/Experiments/Ed25519.o: src/Experiments/Ed25519.hs + ( cd src/Experiments && ghc -XStrict -O3 Ed25519.hs ) -src/Experiments/X25519.o src/Experiments/X25519.core: src/Experiments/X25519.hs - ( cd src/Experiments && ghc -XStrict -O3 X25519.hs -ddump-simpl > X25519.core ) +src/Experiments/X25519.o: src/Experiments/X25519.hs + ( cd src/Experiments && ghc -XStrict -O3 X25519.hs ) extraction: src/Experiments/Ed25519.hs src/Experiments/X25519.hs ghc: src/Experiments/Ed25519.core src/Experiments/Ed25519.o src/Experiments/X25519.o src/Experiments/X25519.core diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index eaa00bea4..5a879f789 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -246,6 +246,7 @@ Extract Inlined Constant Word64.word64 => "Data.Word.Word64". Extract Inlined Constant GF25519BoundedCommon.word64 => "Data.Word.Word64". Extract Inlined Constant GF25519BoundedCommon.w64eqb => "(Prelude.==)". Extract Inlined Constant Word64.word64ToZ => "Prelude.fromIntegral". +Extract Inlined Constant Word64.ZToWord64 => "Prelude.fromIntegral". Extract Inlined Constant GF25519BoundedCommon.word64ToZ => "Prelude.fromIntegral". Extract Inlined Constant GF25519BoundedCommon.NToWord64 => "Prelude.fromIntegral". Extract Inlined Constant GF25519BoundedCommon.ZToWord64 => "Prelude.fromIntegral". |