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/CompleteEdwardsCurve | |
| 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/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 8ef1b95d4..3740f5a29 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -4,7 +4,7 @@ Require Import Crypto.ModularArithmetic.FField. Require Import Crypto.ModularArithmetic.FNsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Eqdep_dec. +Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. Section CompleteEdwardsCurveTheorems. diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v index 7c1e173ee..84c1289f6 100644 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v @@ -1,7 +1,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.BoundedIterOp. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import BinNums NArith Nnat ZArith. +Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Section EdwardsDoubleAndAdd. Context {prm:TwistedEdwardsParams}. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index e4dc140e1..fea4a99b3 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,4 +1,4 @@ -Require Import BinInt Znumtheory VerdiTactics. +Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. |