diff options
Diffstat (limited to 'src/hls/CondElimproof.v')
| -rw-r--r-- | src/hls/CondElimproof.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v index 565adb1..7e6e035 100644 --- a/src/hls/CondElimproof.v +++ b/src/hls/CondElimproof.v @@ -310,6 +310,12 @@ Qed. Definition match_prog (p: program) (tp: program) := Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp. +Lemma transf_program_match: + forall prog, match_prog prog (transf_program prog). +Proof. + intros. eapply Linking.match_transform_program_contextual. auto. +Qed. + Section CORRECTNESS. Context (prog tprog : program). |