From 64e7c075685d3653d67de29f2c5bc6f2bb1c47ae Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 23 Oct 2019 15:41:43 +0200 Subject: An alternative proof where the match_state does not depend on the translation --- backend/Duplicate.v | 7 ------- 1 file changed, 7 deletions(-) (limited to 'backend/Duplicate.v') diff --git a/backend/Duplicate.v b/backend/Duplicate.v index d1458bd4..a00ef71f 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -222,13 +222,6 @@ Proof. repeat (split; try reflexivity). Qed. -Remark transf_function_aux_fnsig: forall f xf, transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). - Proof. apply transf_function_aux_preserves. Qed. -Remark transf_function_aux_fnparams: forall f xf, transf_function_aux f = OK xf -> fn_params f = fn_params (fn_RTL xf). - Proof. apply transf_function_aux_preserves. Qed. -Remark transf_function_aux_fnstacksize: forall f xf, transf_function_aux f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). - Proof. apply transf_function_aux_preserves. Qed. - Definition transf_function (f: function) : res function := do xf <- transf_function_aux f; OK (fn_RTL xf). -- cgit