From 7052a8e11a0512755eb860f25775b2bcb692fbfb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 9 Nov 2016 14:55:37 -0500 Subject: 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.) --- src/Experiments/Ed25519Extraction.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Experiments') 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. -- cgit v1.2.3