From ecd5a00f5a386a7993bf335f2b10d714f09e444b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 Oct 2021 21:07:15 +0100 Subject: [sched] Remove unnecessary imports --- src/hls/HashTree.v | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'src/hls') diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index 0aa0dd9..f3c57a8 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -16,20 +16,9 @@ * along with this program. If not, see . *) -Require Import compcert.backend.Registers. -Require Import compcert.common.AST. -Require Import compcert.common.Globalenvs. -Require Import compcert.common.Memory. -Require Import compcert.common.Values. -Require Import compcert.lib.Floats. -Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. -Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlock. -Require Import vericert.hls.RTLPar. -Require Import vericert.hls.RTLBlockInstr. #[local] Open Scope positive. -- cgit