coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq Extraction and String

From: Gregory Malecha <gmalecha AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Coq Extraction and String
Date: Wed, 19 Nov 2008 00:08:22 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:reply-to:user-agent:mime-version:to:subject :content-type:content-transfer-encoding:from; b=t28ay4WvAaq/A3EOZizF+SieQSsPetgK4PXnvH8JexaSXhR6YCnXjvZyfMxDZXYQuG OZGIts/C6aVdVCxVyF+sazqNuS5Mi+6cwQm5SWidIq6eL8Ygu6vRAHUu5b6PgC1gUQYq 8auLX3/BiuQ5mRRlPkJLJodmSSa9PQy6Gy5ck=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

I'm working on using Coq extraction but I've run into problems with the string type. If I do

Recursive Extraction Library String.

I get the coq string library, but the name String conflicts with the ocaml String library so when I link my code it can't resolve references. Does anyone know how to fix this in a modular way? Do I need to tell Coq to extract the Coq string library as something like CoqString and then add some sort of command to my extraction script to make sure that it changes the type appropriately everywhere?

Thanks for any help.

--
gregory malecha
gmalecha AT fas.harvard.edu
computer science

[Coq-Club] Coq Extraction and String, Gregory Malecha
- Re: [Coq-Club] Coq Extraction and String, Xavier Leroy