From 4d883322317116f4234d02aae1c101f616f564c6 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Wed, 22 Jun 2016 13:22:16 -0400 Subject: Fix build process --- src/Assembly/AlmostQhasm.v | 2 +- src/Assembly/Pipeline.v | 3 +-- src/Assembly/PseudoConversion.v | 4 ++-- src/Assembly/Qhasm.v | 2 +- src/Assembly/StringConversion.v | 3 +-- 5 files changed, 6 insertions(+), 8 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v index 5a3f1beea..f3ed925c7 100644 --- a/src/Assembly/AlmostQhasm.v +++ b/src/Assembly/AlmostQhasm.v @@ -1,4 +1,4 @@ -Require Import QhasmEvalCommon. +Require Import QhasmCommon QhasmEvalCommon. Require Import Language. Require Import List. diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 949bebade..58215cdf2 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -1,10 +1,9 @@ - Require Import QhasmCommon QhasmEvalCommon. Require Import Pseudo Qhasm AlmostQhasm Conversion Language. Require Import PseudoConversion AlmostConversion StringConversion. Module Pipeline. - Export Util AlmostQhasm Qhasm QhasmString. + Export AlmostQhasm Qhasm QhasmString. Export Pseudo. Transparent Pseudo.Program AlmostQhasm.Program Qhasm.Program QhasmString.Program. diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v index 65c80a960..35f8e1e30 100644 --- a/src/Assembly/PseudoConversion.v +++ b/src/Assembly/PseudoConversion.v @@ -1,10 +1,10 @@ -Require Export Language Conversion QhasmEvalCommon QhasmUtil. +Require Export Language Conversion QhasmCommon QhasmEvalCommon QhasmUtil. Require Export Pseudo AlmostQhasm State. Require Import Bedrock.Word NArith NPeano Euclid. Require Import List Sumbool Vector. Module PseudoConversion <: Conversion Pseudo AlmostQhasm. - Import AlmostQhasm EvalUtil ListState Util Pseudo ListNotations. + Import AlmostQhasm EvalUtil ListState Pseudo ListNotations. Section Conv. Variable w: nat. diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v index 8dd2b9e78..9ba2c0a56 100644 --- a/src/Assembly/Qhasm.v +++ b/src/Assembly/Qhasm.v @@ -1,4 +1,4 @@ -Require Import QhasmEvalCommon. +Require Import QhasmCommon QhasmEvalCommon. Require Import Language. Require Import List NPeano. diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v index f3ff40ff7..c365c5824 100644 --- a/src/Assembly/StringConversion.v +++ b/src/Assembly/StringConversion.v @@ -1,5 +1,5 @@ Require Export Language Conversion. -Require Export String Ascii Basics. +Require Export String Ascii Basics Sumbool. Require Import QhasmCommon QhasmEvalCommon QhasmUtil Qhasm. Require Import NArith NPeano. Require Export Bedrock.Word. @@ -54,7 +54,6 @@ Module StringConversion <: Conversion Qhasm QhasmString. Section Elements. Local Open Scope string_scope. - Import Util. Definition nameSuffix (n: nat): string := (nToHex (N.of_nat n)). -- cgit v1.2.3