diff options
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 bc0f0815..064297f1 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 |