diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-09 14:55:37 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-09 14:59:07 -0500 |
| commit | 7052a8e11a0512755eb860f25775b2bcb692fbfb (patch) | |
| tree | a789b162edb25fd777aeefa09b48922fbbcb6523 /src/Experiments | |
| parent | a1bbca9ca7fb78231166661cdd950103a957303d (diff) | |
Rewrite cast_word so that it's extracted better
It will now be extracted as the identity function automatically, so we
don't need to manually extract it as the empty string.
This should also fix #93. (I think the issue was that this was an
instance of https://coq.inria.fr/bugs/show_bug.cgi?id=4243.)
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. |