diff options
Diffstat (limited to 'src/hls/IfConversion.v')
| -rw-r--r-- | src/hls/IfConversion.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 1879205..2516109 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -30,10 +30,14 @@ Require Import vericert.bourdoncle.Bourdoncle. Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N). -(** * If-Conversion - -This conversion is a verified conversion from RTLBlock back to itself, which performs if-conversion -on basic blocks to make basic blocks larger. *) +(*| +============= +If-Conversion +============= + +This conversion is a verified conversion from RTLBlock back to itself, which +performs if-conversion on basic blocks to make basic blocks larger. +|*) Definition combine_pred (p: pred_op) (optp: option pred_op) := match optp with |