The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

Hello,
I've got a real example which reduces to this one:

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?

-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France