diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-22 16:43:14 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-22 16:43:14 +0200 |
commit | 6adfc52c130ee73cf6ee2ee8b85ed8b5e5024a4a (patch) | |
tree | 39245075fd0da13a3753d331663fff0e080a16c2 /scheduling/BTL_SEsimuref.v | |
parent | acb491500b060fdb0fae74a1ec76480b014dba0c (diff) | |
download | compcert-kvx-6adfc52c130ee73cf6ee2ee8b85ed8b5e5024a4a.tar.gz compcert-kvx-6adfc52c130ee73cf6ee2ee8b85ed8b5e5024a4a.zip |
branches expansions support
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 . |