diff options
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index 20a76f17f..eaa00bea4 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -233,7 +233,7 @@ Extraction Implicit Word.split1 [ 2 ]. Extraction Implicit Word.split2 [ 2 ]. Extraction Implicit WordUtil.cast_word [1 2 3]. Extraction Implicit WordUtil.wfirstn [ 2 4 ]. -Extract Inlined Constant WordUtil.cast_word => "". +Extraction Inline WordUtil.cast_word. Extract Inductive Word.word => "[Prelude.Bool]" [ "[]" "(:)" ] "(\fWO fWS w -> {- match_on_word -} case w of {[] -> fWO (); (b:w') -> fWS b w' } )". @@ -296,4 +296,4 @@ True Import Crypto.Spec.MxDH. Extraction Inline MxDH.ladderstep MxDH.montladder. -Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
\ No newline at end of file +Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519. |