diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-10 20:07:29 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-11 10:45:50 +0200 |
| commit | 95b6814a1cff386150a7573cb30e9cb68a18052c (patch) | |
| tree | 6554b879ef83f510dd984c13c857430fbfe2c732 /scheduling/BTL.v | |
| parent | 895470548b89f00111d1f98ae52d217b9fd15643 (diff) | |
| download | compcert-kvx-95b6814a1cff386150a7573cb30e9cb68a18052c.tar.gz compcert-kvx-95b6814a1cff386150a7573cb30e9cb68a18052c.zip | |
prove sexec_exact
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index a87f674b..476e71a7 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -153,7 +153,7 @@ Inductive state : Type := state. (** outcome of a block execution *) -Record outcome := { +Record outcome := out { _rs: regset; _m: mem; _fin: option final |