From bb6d1cb9e5dea833adf07689df0864178732a494 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 10 Mar 2016 13:49:01 -0500
Subject: 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
```
---
 src/Spec/EdDSA.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/Spec/EdDSA.v')

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 45950f6a1..6f57d7bec 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -4,8 +4,8 @@ Require Import Crypto.Spec.CompleteEdwardsCurve.
 
 Require Import Crypto.Util.WordUtil.
 Require Bedrock.Word.
-Require Znumtheory BinInt.
-Require NPeano.
+Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
+Require Coq.Numbers.Natural.Peano.NPeano.
 
 Coercion Word.wordToNat : Word.word >-> nat.
 
-- 
cgit v1.2.3