diff options
Diffstat (limited to 'x86/Conventions1.v')
| -rw-r--r-- | x86/Conventions1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/x86/Conventions1.v b/x86/Conventions1.v index e3c51f60..a4e3b970 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -423,7 +423,7 @@ Proof. unfold forall_rpair; destruct p; intuition auto. Qed. -Hint Resolve loc_arguments_acceptable: locs. +Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. |