From 3eab786d92b348c1dec33640eec3a02a5a86606b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Sep 2016 11:22:45 -0700 Subject: Fully qualify [Require]s This way they won't become ambiguous if we add new files --- src/Spec/EdDSA.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 25109bc4c..38dc64cef 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -13,7 +13,7 @@ Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Module Import Notations. Import NPeano Nat. - + Infix "^" := pow. Infix "mod" := modulo (at level 40, no associativity). Infix "++" := Word.combine. @@ -64,7 +64,7 @@ Section EdDSA. Local Arguments H {n} _. Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing). - Require Import Omega. + Require Import Coq.omega.Omega. Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega. Program Definition curveKey (sk:secretkey) : nat := @@ -90,4 +90,4 @@ Section EdDSA. ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat), S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A -> valid message (Eenc A) (Eenc R ++ Senc S). -End EdDSA. \ No newline at end of file +End EdDSA. -- cgit v1.2.3