diff options
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index da024a25..0e9c58b3 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1585,7 +1585,7 @@ Lemma find_function_translated: /\ Genv.find_funct_ptr tge bf = Some tf /\ transf_fundef f = OK tf. Proof. - intros until f; intros AG [bound [_ []]] FF. + intros until f; intros AG [bound [_ [?????]]] FF. destruct ros; simpl in FF. - exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. rewrite Genv.find_funct_find_funct_ptr in FF. |