diff options
Diffstat (limited to 'powerpc/Selectionproof.v')
| -rw-r--r-- | powerpc/Selectionproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v index 6d62979..5e0b2b2 100644 --- a/powerpc/Selectionproof.v +++ b/powerpc/Selectionproof.v @@ -1350,11 +1350,11 @@ Proof. constructor; auto. destruct b; auto. (* Sreturn None *) econstructor; split. - econstructor. rewrite <- H; reflexivity. + econstructor. constructor; auto. apply call_cont_commut. (* Sreturn Some *) econstructor; split. - econstructor. simpl. auto. eauto with evalexpr. + econstructor. simpl. eauto with evalexpr. constructor; auto. apply call_cont_commut. (* Sgoto *) econstructor; split. |