diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-10-23 15:41:43 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-10-23 15:41:43 +0200 |
| commit | 64e7c075685d3653d67de29f2c5bc6f2bb1c47ae (patch) | |
| tree | b0557539e8b43847eab459917fedf0369479922a /backend/Duplicate.v | |
| parent | cb7d444a5a97626a794f2167c2a4bc4d51f4ed67 (diff) | |
| download | compcert-kvx-64e7c075685d3653d67de29f2c5bc6f2bb1c47ae.tar.gz compcert-kvx-64e7c075685d3653d67de29f2c5bc6f2bb1c47ae.zip | |
An alternative proof where the match_state does not depend on the translation
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 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). |