The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Paolo Herms wrote:
> Definition True2  := True.
> Definition def (u:unit) (P: Prop) := P.
> Lemma lem u: def u True ->  True2.
>    auto.
> Save.
> Hint Unfold def.
> Hint Resolve lem.
> Goal True2.
>    eauto.
> Fail Save.
>
> I think the call to eauto shouldn't do anything here, as it cannot completely
> solve the goal. Or are there situations where you want this behaviour?
>    

But it _does_ solve the goal!  By asking [Hint Unfold def], you enable 
[eauto] to solve any [def _ True] goal by [constructor].  The proof is 
complete with any value filled in for the unknown [unit].  Undetermined 
unification variables never block [eauto], so you would probably have a 
hard time explaining a heuristic that would stop this case but keep the 
accepted behavior of [eauto].