From bb6d1cb9e5dea833adf07689df0864178732a494 Mon Sep 17 00:00:00 2001 From: Jason Gross 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/BaseSystem.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/BaseSystem.v') diff --git a/src/BaseSystem.v b/src/BaseSystem.v index f0e0db077..4e07c4564 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Local Open Scope Z. -- cgit v1.2.3