diff options
Diffstat (limited to 'src/hls/IfConversion.v')
| -rw-r--r-- | src/hls/IfConversion.v | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 4585770..9b8f4d4 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -30,14 +30,10 @@ Require Import vericert.bourdoncle.Bourdoncle. Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N). -(*| -============= -If conversion -============= +(** * 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. -|*) +on basic blocks to make basic blocks larger. *) Definition combine_pred (p: pred_op) (optp: option pred_op) := match optp with |