From 5089872d20c9e3089676c9267a6394e99cca5121 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Sat, 23 May 2015 12:22:48 -0700
Subject: Add efficient extraction of [nat], [Z], and [string] to Haskell

This mirrors the existing extraction libraries for OCaml.

One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char.  Coq has no way to add extra import
statements to the extracted code.  So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189

Message to github robot: this commit closes #65
---
 plugins/extraction/vo.itarget | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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

diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f04890480f..9c30c5eb3e 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,11 @@
 ExtrHaskellBasic.vo
+ExtrHaskellNatNum.vo
+ExtrHaskellNatInt.vo
+ExtrHaskellNatInteger.vo
+ExtrHaskellZNum.vo
+ExtrHaskellZInt.vo
+ExtrHaskellZInteger.vo
+ExtrHaskellString.vo
 ExtrOcamlBasic.vo
 ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
@@ -6,4 +13,4 @@ ExtrOcamlNatInt.vo
 ExtrOcamlNatBigInt.vo
 ExtrOcamlZInt.vo
 ExtrOcamlZBigInt.vo
-ExtrOcamlString.vo
\ No newline at end of file
+ExtrOcamlString.vo
-- 
cgit v1.2.3