diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-08 11:22:45 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-08 11:22:45 -0700 |
| commit | 3eab786d92b348c1dec33640eec3a02a5a86606b (patch) | |
| tree | 91adbd9562c3a952b1714245cc4e64dcccda2f16 /src/Spec | |
| parent | 054752ccf0b80bc413e70202a823fd034db6ea6b (diff) | |
Fully qualify [Require]s
This way they won't become ambiguous if we add new files
Diffstat (limited to 'src/Spec')
| -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. |