diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-17 17:14:43 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-10-17 18:16:14 -0400 |
| commit | 1a0bd0a5fbd5c44befebb67d7d034f5e7bb7dee5 (patch) | |
| tree | ee2175e4aa06e487eaf0403307fad4d848384e75 /src/Specific/SC25519.v | |
| parent | d9b2ce735b3e6c2afd61df4604098930a7c85e5f (diff) | |
Fix missing imports
Diffstat (limited to 'src/Specific/SC25519.v')
| -rw-r--r-- | src/Specific/SC25519.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Specific/SC25519.v b/src/Specific/SC25519.v index 596945bee..c7206c9e3 100644 --- a/src/Specific/SC25519.v +++ b/src/Specific/SC25519.v @@ -7,6 +7,7 @@ Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.WordUtil. Import NPeano. @@ -16,6 +17,7 @@ Local Notation eta x := (fst x, snd x). Local Notation eta3 x := (eta (fst x), snd x). Local Notation eta4 x := (eta3 (fst x), snd x). Local Notation eta4' x := (eta (fst x), eta (snd x)). +Local Open Scope Z_scope. Section Z. Definition SRep := Z. (*tuple x86.W (256/n).*) |