aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Renumberproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Renumberproof.v')
-rw-r--r--backend/Renumberproof.v8
1 files changed, 1 insertions, 7 deletions
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 09faa131..33d6aafa 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -198,13 +198,7 @@ Proof.
(* builtin *)
econstructor; split.
eapply exec_Ibuiltin; eauto.
- eapply external_call_symbols_preserved; eauto.
- exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
- constructor; auto. eapply reach_succ; eauto. simpl; auto.
-(* annot *)
- econstructor; split.
- eapply exec_Iannot; eauto.
- eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+ eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
eapply external_call_symbols_preserved; eauto.
exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
constructor; auto. eapply reach_succ; eauto. simpl; auto.