From 2ccfaa9cbb2b45adb7368afd329f743a9b10b04b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 14 Mar 2021 11:33:58 +0000 Subject: Fix Verilog imports --- src/hls/Verilog.v | 34 ++++++++++++++++++++-------------- 1 file changed, 20 insertions(+), 14 deletions(-) (limited to 'src') diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index ec1d307..1e4be92 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -17,23 +17,29 @@ * along with this program. If not, see . *) -From Coq Require Import - Structures.OrderedTypeEx - FSets.FMapPositive - Program.Basics - PeanoNat - ZArith - Lists.List - Program. - -Require Import Lia. +Require Import Coq.Structures.OrderedTypeEx. +Require Import Coq.FSets.FMapPositive. +Require Import Coq.Program.Basics. +Require Import Coq.Arith.PeanoNat. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.Program.Program. +Require Import Coq.micromega.Lia. + +Require compcert.common.Events. +Require Import compcert.lib.Integers. +Require Import compcert.common.Errors. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Globalenvs. + +Require Import vericert.common.Vericertlib. +Require Import vericert.common.Show. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.Array. Import ListNotations. -From vericert Require Import Vericertlib Show ValueInt AssocMap Array. -From compcert Require Events. -From compcert Require Import Integers Errors Smallstep Globalenvs. - Local Open Scope assocmap. Set Implicit Arguments. -- cgit