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/Util/ListUtil.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/Util/ListUtil.v')

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 783e3f527..1f9a62457 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1,7 +1,7 @@
-Require Import List.
-Require Import Omega.
-Require Import Arith.Peano_dec.
-Require Import VerdiTactics.
+Require Import Coq.Lists.List.
+Require Import Coq.omega.Omega.
+Require Import Coq.Arith.Peano_dec.
+Require Import Crypto.Tactics.VerdiTactics.
 
 Ltac boring :=
   simpl; intuition;
-- 
cgit v1.2.3