diff options
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 4420269..79657c5 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -765,13 +765,13 @@ Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). Lemma funct_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog). +Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). Lemma sig_translated: forall (f: RTL.fundef), |