diff options
| author | Pierre Nigron <pierre.nigron@free.fr> | 2020-09-22 12:32:59 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-19 16:23:17 +0200 |
| commit | b816d696733c96fdc62428e43c4a4a1f5a09b47b (patch) | |
| tree | 7a6ed23ab65addb874852d30b3a6ed8f1be11820 /backend/RTLgenproof.v | |
| parent | 88cccb19502dfec65f7e21d0f6772ba99b1fb99d (diff) | |
| download | compcert-b816d696733c96fdc62428e43c4a4a1f5a09b47b.tar.gz compcert-b816d696733c96fdc62428e43c4a4a1f5a09b47b.zip | |
RTLgen: use the state and error monad for reserve_labels (#371)
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 5 |
1 files changed, 2 insertions, 3 deletions
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. |