From 4d262face34cb79d478823fd8db32cf02dc187f8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 21 Jun 2023 18:57:33 +0100 Subject: Add SMTCoq solver as dependency --- src/Compiler.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Compiler.v') diff --git a/src/Compiler.v b/src/Compiler.v index 5ff291e..2fb909e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -55,6 +55,7 @@ Require Import compcert.common.Errors. Require Import compcert.common.Linking. Require Import compcert.common.Smallstep. Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Maps. Require vericert.hls.Verilog. Require vericert.hls.Veriloggen. @@ -279,7 +280,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion CondElim.transf_program @@ print (print_GibleSeq 1) - @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (Maps.PTree.empty _ :: Maps.PTree.empty _ :: nil)) + @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (PTree.empty _ :: PTree.empty _ :: nil)) @@ print (print_GibleSeq 2) @@@ DeadBlocks.transf_program @@ print (print_GibleSeq 3) -- cgit