diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-31 20:11:14 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-31 20:11:14 -0500 |
| commit | ee61a83885ab04b259a767aab9932fd97825df3d (patch) | |
| tree | 572f37456da6fee911938e9531c3bc17a628d6f8 | |
| parent | d16174cecc15f74f91644098729f2aed99e97cd3 (diff) | |
Absolutize some imports
| -rw-r--r-- | src/Assembly/Evaluables.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 0678c80bb..924f548fa 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -1,9 +1,9 @@ Require Import Bedrock.Word Bedrock.Nomega. -Require Import NPeano NArith PArith Ndigits ZArith Znat ZArith_dec Ndec. -Require Import List Basics Bool Nsatz Sumbool Datatypes. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.ZArith.ZArith Coq.ZArith.Znat Coq.ZArith.ZArith_dec Coq.NArith.Ndec. +Require Import Coq.Lists.List Coq.Program.Basics Crypto.Util.Bool Crypto.Tactics.Algebra_syntax.Nsatz Coq.Bool.Sumbool Coq.Init.Datatypes. Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. -Require Import QhasmUtil WordizeUtil Bounds. -Require Import ProofIrrelevance. +Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.WordizeUtil Crypto.Assembly.Bounds. +Require Import Coq.Logic.ProofIrrelevance. Import ListNotations. |