From e5034fbbf23edb17dd88175b2f44b2dc9b4110fa Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 4 Jun 2010 20:19:02 +0000
Subject: Extraction: attempt to provide nice extraction of chars and strings
 for Ocaml

 When Requiring ExtrOcamlString :

 * ascii is mapped to Ocaml's char, the ugly translation of constructor
 and pattern-match should hopefully be seen very rarely (never ?).
 We add a hack in ocaml.ml for recognizing constant chars.

 * string is mapped to (list char). Extracting to Ocaml's string could be
 done, but would be really nasty (lots of non-trivial Extract Constant to
 add). For now, (list char) seems a good compromise.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13078 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/vo.itarget | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/extraction/vo.itarget')

diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f7168ff407..338b276840 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -3,3 +3,4 @@ ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
 ExtrOcamlNatInt.vo
 ExtrOcamlNatBigInt.vo
+ExtrOcamlString.vo
\ No newline at end of file
-- 
cgit v1.2.3