From b816d696733c96fdc62428e43c4a4a1f5a09b47b Mon Sep 17 00:00:00 2001 From: Pierre Nigron Date: Tue, 22 Sep 2020 12:32:59 +0200 Subject: RTLgen: use the state and error monad for reserve_labels (#371) --- backend/RTLgenproof.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 79b9319b..90f03c1c 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -397,9 +397,8 @@ Lemma sig_transl_function: Proof. intros until tf. unfold transl_fundef, transf_partial_fundef. case f; intro. - unfold transl_function. - destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0]. - case (transl_fun f0 ngoto s0); simpl; intros. + unfold transl_function. + case (transl_fun f0 (init_state)); simpl; intros. discriminate. destruct p. simpl in H. inversion H. reflexivity. intro. inversion H. reflexivity. -- cgit