diff options
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index c812c607..7af1af62 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -260,11 +260,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop := (RIS: ris_refines ctx ris sis) (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) - | Refcond cond rargs args rifso rifnot ifso ifnot - (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args) - (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) - (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) - : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot) + | Refcond rcond cond rargs args rifso rifnot ifso ifnot + (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args) + (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot) | Refabort : rst_refines ctx Rabort Sabort . |