Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Strict Implicit

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strict Implicit


chronological Thread 
  • From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
  • To: Stephane Le Roux <stephane.le.roux AT ens-lyon.fr>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Strict Implicit
  • Date: Thu, 6 Dec 2007 14:40:19 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.





Archive powered by MhonArc 2.6.16.

Top of Page