From bc0239c0f6f5bafcf264cbabf3d783ca1146360d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 3 Nov 2016 20:25:30 -0400 Subject: separate Ed25519Extraction.v, add extraction to Makefile @JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment --- src/Specific/GF25519Bounded.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Specific/GF25519Bounded.v') diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 0ce49f1c0..2d83b8dbd 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -172,6 +172,7 @@ Proof. exact (proj2_sig (eqbW_sig f' g')). Qed. +(* TODO(jgross): use NToWord or such for this constant too *) Definition sqrt_m1W : fe25519W := Eval vm_compute in fe25519ZToW sqrt_m1. -- cgit v1.2.3