diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 16:02:57 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 16:02:57 +0200 |
| commit | 99e735af1f7726da2903409758bee202cf47c6a4 (patch) | |
| tree | 943b15506d058750c3a4409e915c2daceb282388 /scheduling/BTL.v | |
| parent | 3948e8e02e7a7c72010aebe540c65d6bc984c2b8 (diff) | |
| download | compcert-kvx-99e735af1f7726da2903409758bee202cf47c6a4.tar.gz compcert-kvx-99e735af1f7726da2903409758bee202cf47c6a4.zip | |
Lemmas on ISTEP
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 064297f1..d55a0415 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -819,6 +819,7 @@ Fixpoint expand (ib: iblock) (k: option iblock): iblock := | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) | Bcond cond args ib1 ib2 i => Bcond cond args (expand ib1 k) (expand ib2 k) i + | BF fin => fin | ib => match k with | None => ib |