diff options
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index d5d7e033..bc991f0f 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -400,7 +400,7 @@ Proof. simpl in H0. unfold ge, fundef in H0. rewrite A in H0. rewrite <- Genv.find_funct_ptr_iff in B. congruence. -Qed. +Qed. (** Translation of builtin arguments. *) |