diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 1c2d090..d02aff6 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -107,7 +107,7 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : c c!pc = Some (RTL.Ireturn r) -> (exists pc2, - stmnts!pc = Some (return_val fin rtrn r) /\ + stmnts!pc = Some (do_return fin rtrn r) /\ trans!pc = Some (state_goto st pc2) /\ stmnts!pc2 = Some (idle fin) /\ trans!pc2 = Some Vskip) -> |