From f7a4a67784b97013cd314fb4c50bd94abdb9c55e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 25 Mar 2019 11:14:17 +0100 Subject: RTLgenproof: destruct too deep `external_call_mem_extends` returns a conjunction of 4 properties, but the destruct pattern was 5 level deep. (Reported by Jeremie Koenig in pull request #278.) --- backend/RTLgenproof.v | 4 ++-- 1 file 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 *) -- cgit