diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-03-10 13:49:01 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:42:17 -0400 |
| commit | 1ab15c48f917a937215fd97c64b53e06130ae871 (patch) | |
| tree | 25059c026d0fa5a661cc3c871ffcd184a50682f4 /src/BoundedIterOp.v | |
| parent | 9fa6efa9ef8431b5a81697e2276f1707b3b9fa2f (diff) | |
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
```
Diffstat (limited to 'src/BoundedIterOp.v')
| -rw-r--r-- | src/BoundedIterOp.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |