diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-03-10 13:49:01 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-03-10 13:49:01 -0500 |
| commit | bb6d1cb9e5dea833adf07689df0864178732a494 (patch) | |
| tree | 2e6e1d7befc950131f217633af09d7ac27e9b04b /src/EdDSAProofs.v | |
| parent | dbe09dd5bfc2595cb9fd96725d87d9a729cd0247 (diff) | |
Finish absolutizing imports
The file coqprime/Coqprime/ListAux.v was importing List, which was confusing
machines on which mathclasses was also installed.
Using https://github.com/JasonGross/coq-tools
```bash
make -kj10
cd src
git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto
```
Diffstat (limited to 'src/EdDSAProofs.v')
| -rw-r--r-- | src/EdDSAProofs.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v index 7357284e1..83467bf6d 100644 --- a/src/EdDSAProofs.v +++ b/src/EdDSAProofs.v @@ -1,11 +1,11 @@ Require Import Crypto.Spec.EdDSA Crypto.Spec.Encoding. -Require Import NPeano. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Bedrock.Word. -Require Import Znumtheory BinInt ZArith. +Require Import Coq.ZArith.Znumtheory Coq.ZArith.BinInt Coq.ZArith.ZArith. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import VerdiTactics. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope nat_scope. Section EdDSAProofs. |