diff options
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 38ba38b..ee24187 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -653,13 +653,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 function_ptr_translated: forall (v: block) (f: RTL.fundef), Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = 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), |