coq/plugins/extraction/vo.itarget, branch master

Remove remaining vo.itarget files (obsolete since PR #499)

2017-06-10T14:13:54+00:00

Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."

2017-03-23T13:51:21+00:00

This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is
an 8.6 only commit.

Add empty Extraction.v and FunInd.v to prepare landing of PR#220.

2017-03-23T00:30:43+00:00

This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.

Add efficient extraction of [nat], [Z], and [string] to Haskell

2015-06-22T12:15:00+00:00

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

add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.v

2015-04-08T10:01:30+00:00

Extraction: in support library, more and nicer big_int

2010-06-15T14:28:05+00:00

 - we use a wrapper file big.ml to have short names about big_int
 and specialized functions for extraction
 - new files : ExtrOcamlZInt for Z==>int and N==>int,
 ExtrOcamlZBigInt for Z==>big_int and N==>big_int

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7

Extraction: attempt to provide nice extraction of chars and strings for Ocaml

2010-06-04T20:19:02+00:00

 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

Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int

2010-06-04T13:19:50+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7

Extraction: start of a support library

2010-06-02T15:06:03+00:00

 - ExtrOcamlBasic: mapping of basic types to ocaml's ones
 - ExtrOcamlIntConv: conversion between int and coq's numerical types
 - ExtrOcamlBigIntConv: same with big_int (no overflow)
 - ExtrOcamlNatInt: realizes nat by int (unsafe)

more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt,
etc etc...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7