diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-10-24 11:05:35 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-24 11:05:35 +0200 |
| commit | 3d6c498c1c11ad1b73efe4a0163d17cd8e9b5e86 (patch) | |
| tree | 1daa82bead05b322672e929129415ccfd0542a23 /cfrontend/SimplExprproof.v | |
| parent | 0fca312236475ccc2de12da45221c311d99a19d1 (diff) | |
| parent | 995f654c43092ceb258f7c0799a4101ed6e570af (diff) | |
| download | compcert-3d6c498c1c11ad1b73efe4a0163d17cd8e9b5e86.tar.gz compcert-3d6c498c1c11ad1b73efe4a0163d17cd8e9b5e86.zip | |
Merge pull request #458 from AbsInt/simpl-expr-dests
SimplExpr: revised handling of nested conditional, `||`, `&&` expressions
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index ea89a8ba..2aed0cdf 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1611,7 +1611,7 @@ Ltac NOTIN := apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. + apply S. apply tr_paren_set with (a1 := a2) (t := t); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. - (* seqand false *) exploit tr_top_leftcontext; eauto. clear TR. @@ -1720,7 +1720,7 @@ Ltac NOTIN := apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. + apply S. apply tr_paren_set with (a1 := a2) (t := t); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. - (* condition *) exploit tr_top_leftcontext; eauto. clear TR. |