The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,
 
> In the example below, Coq says that the first argument of a function
> is implicit (despite the command Set Strict Implicit). Then, when
> trying to build a term with the function, Coq says that the first
> argument cannot be inferred. Is this the intended behaviour?

This is a known bug of the strict mode. Next version will come with a
new option "Set Strong Strict Implicit" (!!) to activate the fixed
behaviour while preserving backward compatibility.

Regards,

Hugo Herbelin

PS: as a general rule, please use the bug tracker from
http://coq.inria.fr/contacts-eng.html for bug report.