The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

In his message of Tue July 21, 1998, Pierre CASTERAN writes: 
> 
> Hello,
> 
>   Which is the criterium with respect to which we can use the
> "?" joker for typing ?
> 
Unfortunately, resolution of implicits is somewhat complex and there is
no formal description of the algorithms used in Coq. The criterium is
then : if the algorithm work, keep the "?"; otherwise, put explicitely
the type. Simple, isn't it ?

More seriously, there is some work in the Coq team about implicit
arguments, and it is possible that in the 6.3 resolution of "?"'s will be
improved and the rules of the game easier to understand. However, as I
already said, resolution of implicits is a hard task and there will be
no miracle.

Regards,

-- 
Patrick.Loiseleur AT lri.fr