diff options
Diffstat (limited to 'backend/Tunnelingproof.v')
| -rw-r--r-- | backend/Tunnelingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d3b8a9f0..cdf6c800 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -22,7 +22,7 @@ Definition match_prog (p tp: program) := match_program (fun ctx f tf => tf = tunnel_fundef f) eq p tp. Lemma transf_program_match: - forall p, match_prog p (tunnel_program p). + forall p, match_prog p (transf_program p). Proof. intros. eapply match_transform_program; eauto. Qed. |