From 26d9fbb36b2e9c8f1262250035cd804bf87f7228 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 14 Jun 2021 19:02:39 +0200 Subject: Preparation for scheduling proof, main lemmas ok --- scheduling/RTLtoBTLproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 18ff8d5f..513ed40a 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -375,7 +375,7 @@ Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.f Proof. intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto. erewrite preserv_fnsig; eauto. -Admitted. +Qed. Lemma transf_initial_states s1: RTL.initial_state prog s1 -> -- cgit