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/Util/NumTheoryUtil.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Util/NumTheoryUtil.v') diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 5acef8b75..10ce148b0 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -1,8 +1,8 @@ -Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. Require Import Coqprime.Zp. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z. (* TODO: move somewhere else for lemmas about Coqprime? *) -- cgit v1.2.3