diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:06:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:06:12 +0100 |
| commit | 11dc19dc169d99a944abb4144ea67eb4fc03f883 (patch) | |
| tree | e2302c850109839b7e4bcf890a327cd1f7538ea7 /backend/CSE3analysisproof.v | |
| parent | c2319ee007eba06f92837e1e370dfa5e58b06b82 (diff) | |
| download | compcert-kvx-11dc19dc169d99a944abb4144ea67eb4fc03f883.tar.gz compcert-kvx-11dc19dc169d99a944abb4144ea67eb4fc03f883.zip | |
moved no away
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index e2ce6b5d..a1e57eb5 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -485,10 +485,10 @@ Section SOUNDNESS. sem_rel rel rs m -> sem_rhs sop args rs m v -> ~ In dst args -> - eq_find (ctx := ctx) - no {| eq_lhs := dst; - eq_op := sop; - eq_args:= args |} = Some eqno -> + eq_find (ctx := ctx) no + {| eq_lhs := dst; + eq_op := sop; + eq_args:= args |} = Some eqno -> sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m. Proof. intros until v. |