diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 19:49:46 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 19:49:46 +0200 |
| commit | 780ad9d001af651a49d7470e963ed9a49ee11a4c (patch) | |
| tree | e44c241221c24d6b0e8b241a5a7b305fe96a11f2 /backend/Selectionproof.v | |
| parent | 4c379d48b35e7c8156f3953fede31d5e47faf8ca (diff) | |
| download | compcert-kvx-780ad9d001af651a49d7470e963ed9a49ee11a4c.tar.gz compcert-kvx-780ad9d001af651a49d7470e963ed9a49ee11a4c.zip | |
various fixes
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 622992e5..8a827af2 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1189,12 +1189,12 @@ Proof. (* store *) - unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. rewrite sel_builtin_nolabel; auto. (* tailcall *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* builtin *) - rewrite sel_builtin_nolabel; auto. +- rewrite sel_builtin_nolabel; auto. (* seq *) - exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; |