From 90375dc090b19cf8202903754d7f47e8d568d9f8 Mon Sep 17 00:00:00 2001
From: Pierre Goutagny <pierre.goutagny@ens-lyon.fr>
Date: Mon, 14 Jun 2021 15:37:50 +0200
Subject: Add RTL Tunneling as a pass

---
 backend/RTLTunnelingproof.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'backend/RTLTunnelingproof.v')

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.
-- 
cgit