diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-31 20:12:29 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-31 20:12:29 -0500 |
| commit | 920a40e3d8c14abe30351cf881f089bb63d6868d (patch) | |
| tree | 267312609770998caf49e23d3cce4a6036aec8b6 /src/Assembly | |
| parent | ee61a83885ab04b259a767aab9932fd97825df3d (diff) | |
Absolutize some imports
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/StringConversion.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v index b4bc9c9de..f1ec58dca 100644 --- a/src/Assembly/StringConversion.v +++ b/src/Assembly/StringConversion.v @@ -1,6 +1,6 @@ -Require Export String Ascii Basics Sumbool. -Require Import QhasmCommon QhasmEvalCommon QhasmUtil Qhasm. -Require Import NArith NPeano. +Require Export Coq.Strings.String Coq.Strings.Ascii Coq.Program.Basics Coq.Bool.Sumbool. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Qhasm. +Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano. Require Export Bedrock.Word. Module StringConversion. |