diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-10-03 13:35:47 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-10-03 13:35:47 -0400 |
| commit | e52fd783c8c1dbfc99ff7e9014c4dfa8f3a8d9c8 (patch) | |
| tree | 70e6fd79c4d93a52cb164ca8926fcd78f8d131af /src/Spec | |
| parent | c9ffe0806515c0540caadb65d8fdcf7f72280503 (diff) | |
Ed25519: use Global Instance
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/Ed25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 9598b8881..150e3f388 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -43,8 +43,8 @@ Section Ed25519. Axiom Senc : Fl -> Word.word b. (* TODO(jadep) *) (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) - Axiom prime_q : Znumtheory.prime q. Existing Instance prime_q. - Axiom prime_l : Znumtheory.prime l. Existing Instance prime_l. + Axiom prime_q : Znumtheory.prime q. Global Existing Instance prime_q. + Axiom prime_l : Znumtheory.prime l. Global Existing Instance prime_l. Require Import Crypto.Util.Decidable. Definition ed25519 : |