From 920a40e3d8c14abe30351cf881f089bb63d6868d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Jan 2017 20:12:29 -0500 Subject: Absolutize some imports --- src/Assembly/StringConversion.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Assembly') 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. -- cgit v1.2.3