From 1ab15c48f917a937215fd97c64b53e06130ae871 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/BoundedIterOp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/BoundedIterOp.v') diff --git a/src/BoundedIterOp.v b/src/BoundedIterOp.v index fbdc823ad..bd4f7d66e 100644 --- a/src/BoundedIterOp.v +++ b/src/BoundedIterOp.v @@ -1,5 +1,5 @@ Require Import Crypto.Tactics.VerdiTactics. -Require Import BinNums NArith Nnat ZArith. +Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Definition testbit_rev p i bound := Pos.testbit_nat p (bound - i). -- cgit v1.2.3