The Coq mailing list

["St�phane Lescuyer" <stephane.lescuyer AT polytechnique.org>]

Well, extraction is indeed tagged as 'experimental' in the
documentation, but it would agree with you nonetheless. I am actually
using extraction on a rather big Coq project and it works perfectly
(except a couple of glitches that were corrected by Pierre anyway).

Stéphane

On Fri, Nov 7, 2008 at 2:15 PM, Adam Chlipala 
<adamc AT hcoop.net>
 wrote:
> AUGER Cédric wrote:
>>
>> Extraction is still experimental
>
> Really?  I've been thinking of it as one of the most core, well-established
> features of Coq.  I've used it since 7.something.
>
> Is there some new reimplementation that might have introduced regression
> bugs?
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06