diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-02-25 13:56:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-02-25 13:56:59 +0000 |
| commit | 8d71333042d9ed87a80cffd4005daa0a0acc1810 (patch) | |
| tree | 1453227ec7a8231d6c8e5c3050bc4af382138fa9 /src/hls/IfConversion.v | |
| parent | c1c5fc8e12342a9fe435c8066c8e9316036ff991 (diff) | |
| download | vericert-8d71333042d9ed87a80cffd4005daa0a0acc1810.tar.gz vericert-8d71333042d9ed87a80cffd4005daa0a0acc1810.zip | |
Start converting comments
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 |