From 780ad9d001af651a49d7470e963ed9a49ee11a4c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 19:49:46 +0200 Subject: various fixes --- backend/Selectionproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Selectionproof.v') 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] | ]; -- cgit