The Coq mailing list

[Martin Bodin <martin.bodin AT inria.fr>]

> And what happens when you are trying:
>
> Definition test : A -> B -> C := fun a => proj1 T.
> Does it take a long time ?

Hi,
Yes! It does take the “same” (I didn't see it terminate) amount of time. 
I thus guess that the “exact” tactic does less work than I thought.

I'm afraid that Gregory Malecha is right: I'll work on a minimalistic 
example runnable without library… and trying to add explicit types to 
the problematic terms.

Thanks a lot for your help! I've learned about “Qed” ;-)
Martin.