diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-12 15:42:21 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-12 15:42:21 +0100 |
| commit | 4c87dd36bb8ac1a50b62d73d4d6e381093a97357 (patch) | |
| tree | 7ec0d4e53b37ccf3aba87d1038261637acb80fcb /src/hls/RTLBlockInstr.v | |
| parent | ab45ed9114d805693cbe7637c0bc5fa65e0a10c5 (diff) | |
| download | vericert-4c87dd36bb8ac1a50b62d73d4d6e381093a97357.tar.gz vericert-4c87dd36bb8ac1a50b62d73d4d6e381093a97357.zip | |
Up to Icall is now proven
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 5e61b99..2d48650 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -354,7 +354,7 @@ Section RELSEM. eval_predf (is_ps i) p = false -> eval_pred (Some p) i i' i | eval_pred_none: - forall i i', eval_pred None i i' i. + forall i i', eval_pred None i i' i'. (*| .. index:: |