aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/StringConversion.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Assembly/StringConversion.v')
-rw-r--r--src/Assembly/StringConversion.v6
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.