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/WordUtil.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/WordUtil.v') diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 49de971ef..17d04c60a 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1,5 +1,5 @@ -Require Import NPeano. -Require Import ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.ZArith.ZArith. Require Import Bedrock.Word. Local Open Scope nat_scope. -- cgit v1.2.3