diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Selectionproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v index e487d15a..a307597a 100644 --- a/arm/Selectionproof.v +++ b/arm/Selectionproof.v @@ -1427,11 +1427,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. |