Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.


chronological Thread 
  • From: Claudio Sacerdoti Coen <sacerdot AT CS.UniBO.IT>
  • To: coq-club AT pauillac.inria.fr, veronique.benzaken AT lri.fr, Giuseppe.Castagna AT ens.fr, frisch AT clipper.ens.fr, Marwan.Burelle AT lri.fr
  • Subject: Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.
  • Date: Tue, 11 Feb 2003 16:47:58 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

 Dear Serge,

On Tue, Feb 11, 2003 at 15:05:08 +0100, Serge Leblanc wrote:
> Hello, for my first contribution I wish to
> carry out a Coq->CDuce[1] extraction functionality.

 what do you want to extract exactly?

> Before starting I would like to know if somebody does not 
> already carry out this.

 Depending on what do you want to extract, it may be a good
 idea to either:

 1. start from the extracted XML files.
    [The extraction module to XML is already part of the standard
     distribution of Coq, but it is undocumented. (Some small
     parts will change again in a few monthes. Other are really
     stable.) Feel free to ask me more infos about that.]
 2. modify the extraction module for XML files.
    [More difficult than 1, IMHO.]
 3. restart from scratch if the information you need is not there.
    [In this case I would be interested in privately know what
     is the missing information.]

                                        Regards,
                                        C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://caristudenti.cs.unibo.it/~sacerdot
----------------------------------------------------------------




Archive powered by MhonArc 2.6.16.

Top of Page