From 2f313b9ced2e74702e4881f858cbebb205b2cdd5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 22 Jan 2021 17:20:34 +0000 Subject: Fix types with new changes in RTLBlock Also formatted some files so that they are under 80 columns, which is much nicer to read. --- src/hls/RTLBlock.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/hls/RTLBlock.v') diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 32d7674..2a388e6 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -31,8 +31,9 @@ Require Import compcert.verilog.Op. Require Import vericert.hls.RTLBlockInstr. Definition bblock_body : Type := list instr. +Definition bblock := bblock bblock_body. -Definition code : Type := PTree.t (@bblock bblock_body). +Definition code : Type := PTree.t bblock. Record function: Type := mkfunction { fn_sig: signature; -- cgit