diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-24 11:15:43 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-24 11:15:43 +0200 |
| commit | edf0180351f7fbdb129f1f5f1debf3a66a478cda (patch) | |
| tree | b60d38ed4ab2189beb51a3b1280b6d8714281538 /backend/Duplicate.v | |
| parent | 8bee1136d7d298e9f33ea91ee7a248909467dd13 (diff) | |
| parent | 64e7c075685d3653d67de29f2c5bc6f2bb1c47ae (diff) | |
| download | compcert-kvx-edf0180351f7fbdb129f1f5f1debf3a66a478cda.tar.gz compcert-kvx-edf0180351f7fbdb129f1f5f1debf3a66a478cda.zip | |
Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-work
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 68a7f413..a591d6e5 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). |