Why doesn't Coq accept this lemma as a hint?
Lemma contr : forall p1 : Prop, False -> p1.
Proof. tauto. Qed.
Hint Resolve contr : Hints.
Or other lemmas that end with a Prop variable?
Looking at the documentation for Hint Resolve ( http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@command232 ):
term cannot be used as a hint
The type of term contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the apply tactic fails, and thus is useless.
However, it does not seem (to me) to be the case here, as the only product is over p1 which does appear in the conclusion.
The problem here seems to be that your conclusion have absolutely no shape at all. auto seems to work by matching the shape of your goal with the shape of the return type of the hint database. Here, it might be upset by the fact that your goal is just a quantified variable. I am not sure whether this is a reasonable thing to trip over, but this particular instance might be the only case where you might have such a shapeless return type (with obviously the same case for Set and Type), so it's not a big deal.
So, you probably don't need this as a hint?... just use tactics such as tauto, intuition or perform any kind of elimination/destruction/inversion on the value of type False in your environment... not very satisfactory but eh :\