diff options
| author | Pierre Goutagny <pierre.goutagny@ens-lyon.fr> | 2021-06-14 15:37:50 +0200 |
|---|---|---|
| committer | Pierre Goutagny <pierre.goutagny@ens-lyon.fr> | 2021-06-14 15:37:50 +0200 |
| commit | 90375dc090b19cf8202903754d7f47e8d568d9f8 (patch) | |
| tree | 0b98a0fa4c4588cd8a787d70f45b0468798beaf8 /backend/RTLTunnelingproof.v | |
| parent | 77d1ab5f7a6d04970185102508f1cec529c7cb40 (diff) | |
| download | compcert-kvx-90375dc090b19cf8202903754d7f47e8d568d9f8.tar.gz compcert-kvx-90375dc090b19cf8202903754d7f47e8d568d9f8.zip | |
Add RTL Tunneling as a pass
Diffstat (limited to 'backend/RTLTunnelingproof.v')
| -rw-r--r-- | backend/RTLTunnelingproof.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 7f6696ad..14a2c037 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -149,6 +149,11 @@ Definition match_prog (p tp: program) := * `p` et `tp` sont les programmes donc on doit dire s'ils match *) + (**) Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. Section PRESERVATION. |