aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLParFUgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/RTLParFUgen.v')
-rw-r--r--src/hls/RTLParFUgen.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index 65ddf74..49ee6e7 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -161,7 +161,6 @@ Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function :=
(max+6)%positive
(max+4)%positive
(max+5)%positive
- ltac:(lia)
)) initial_resources in
do c' <- transl_code fu (RTLBlockInstr.fn_code f);
Errors.OK (mkfunction (RTLBlockInstr.fn_sig f)