diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-11 10:21:26 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-11 10:21:26 -0500 |
| commit | 11f1d0cc2708aabd875d675ef39e86a1c8547ace (patch) | |
| tree | 774d5d0f19f4a6be8971ff8218281fe2a8ee58d5 /src/Experiments | |
| parent | c19c7aa0b4efa8a2529304d4c4e46435d765699e (diff) | |
extraction less slow
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 1 |
1 files changed, 1 insertions, 0 deletions
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". |