coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Strict Implicit, Stephane Le Roux
- Re: [Coq-Club] Strict Implicit,
Jean-Francois Monin
- Re: [Coq-Club] Strict Implicit, Pierre Castéran
- Re: [Coq-Club] Strict Implicit, Hugo Herbelin
- Re: [Coq-Club] Strict Implicit,
Jean-Francois Monin
Archive powered by MhonArc 2.6.16.