diff options
| -rw-r--r-- | backend/RTLgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b003eb10..b94ec22f 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -704,7 +704,7 @@ Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. exploit external_call_mem_extends; eauto. - intros [v' [tm2 [A [B [C [D E]]]]]]. + intros [v' [tm2 [A [B [C D]]]]]. exists (rs1#rd <- v'); exists tm2. (* Exec *) split. eapply star_right. eexact EX1. @@ -736,7 +736,7 @@ Proof. intros; red; intros. inv TE. exploit H3; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. exploit external_call_mem_extends; eauto. - intros [v' [tm2 [A [B [C [D E]]]]]]. + intros [v' [tm2 [A [B [C D]]]]]. exploit function_ptr_translated; eauto. simpl. intros [tf [P Q]]. inv Q. exists (rs1#rd <- v'); exists tm2. (* Exec *) |