diff options
| -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 : |