aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-07-11 15:59:21 +0200
committerYann Herklotz <git@yannherklotz.com>2021-07-11 15:59:21 +0200
commit178a7c4781c96857fe0a33c777da83e769516152 (patch)
treecf4b5248a144289c84161a6fd73de37523c9d373 /driver
parent3dfc30619a4f3ecf0f262481a0891259c2b37ed1 (diff)
downloadvericert-178a7c4781c96857fe0a33c777da83e769516152.tar.gz
vericert-178a7c4781c96857fe0a33c777da83e769516152.zip
Remove unnecessary files and proofs
Diffstat (limited to 'driver')
-rw-r--r--driver/VericertDriver.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 0706d79..aa5309a 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -93,7 +93,7 @@ let compile_c_file sourcename ifile ofile =
end else begin
let verilog =
let translation = if !option_hls_schedule
- then Vericert.Compiler0.transf_hls_temp
+ then Vericert.Compiler0.transf_hls
else Vericert.Compiler0.transf_hls
in
match translation csyntax with