diff options
Diffstat (limited to 'src/hls/RTLPargen.v')
| -rw-r--r-- | src/hls/RTLPargen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index d425049..214da6f 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -227,7 +227,7 @@ We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling transformation. |*) -Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := +Definition empty_trees (bb: list RTLBlock.bb) (bbt: list RTLPar.bb) : bool := match bb with | nil => match bbt with |