diff options
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 457f0d1..49d3ff3 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1525,11 +1525,10 @@ Proof. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. eapply transl_fundef_sig1; eauto. - rewrite H3. rewrite H. auto. + rewrite H3. auto. econstructor; eauto. econstructor; eauto. simpl. auto. - rewrite H3; rewrite H; eauto. eapply eval_exprlist_casted; eauto. (* seq *) |