aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3916.v
blob: 9d8da11017e93454461281f9ff60d47520c38480 (plain)
1
2
Require Import List.
Fail Hint Resolve -> in_map.