diff options
Diffstat (limited to 'src/Spec/EdDSA.v')
| -rw-r--r-- | src/Spec/EdDSA.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |