From e52fd783c8c1dbfc99ff7e9014c4dfa8f3a8d9c8 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 3 Oct 2016 13:35:47 -0400 Subject: Ed25519: use Global Instance --- src/Spec/Ed25519.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Spec') 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 : -- cgit v1.2.3