diff options
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 0a77b19..c907f77 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1003,7 +1003,7 @@ Proof. end). { induction 1; simpl; intros. auto. - destruct c; auto. destruct (Int.eq i n); auto. + destruct c; auto. destruct (zeq z n); auto. econstructor; split; eauto. constructor; auto. } intros. unfold Csem.select_switch, select_switch. specialize (CASE n ls tls H). @@ -2113,7 +2113,7 @@ Proof. left; eapply plus_left. constructor. apply push_seq. traceEq. econstructor; eauto. constructor; auto. (* expr switch *) - inv H7. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + inv H8. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left; eapply plus_two. constructor. econstructor; eauto. traceEq. econstructor; eauto. |