diff options
Diffstat (limited to 'backend/Deadcodeproof.v')
| -rw-r--r-- | backend/Deadcodeproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 7aa6ff88..7be12c69 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -358,7 +358,7 @@ Proof. intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto. Qed. -Hint Resolve add_need_all_eagree add_need_all_lessdef +Global Hint Resolve add_need_all_eagree add_need_all_lessdef add_need_eagree add_need_vagree add_needs_all_eagree add_needs_all_lessdef add_needs_eagree add_needs_vagree |