coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Guide to Coq Sources

From: Adam Chlipala <adamc AT hcoop.net>
To: Cedric.Auger AT lri.fr
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Guide to Coq Sources
Date: Fri, 07 Nov 2008 08:15:01 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

Re: [Coq-Club] Guide to Coq Sources, Ashish Darbari
- Re: [Coq-Club] Guide to Coq Sources, AUGER C�dric
  - Re: [Coq-Club] Guide to Coq Sources, Adam Chlipala
    - Re: [Coq-Club] Guide to Coq Sources, St�phane Lescuyer
      - Re: [Coq-Club] Guide to Coq Sources, Pierre Letouzey