coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\|
*	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès	2017-03-23
\| \| \| \| \|	This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
*	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès	2017-03-23
\| \| \| \| \|	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	Nickolai Zeldovich	2015-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	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	Nickolai Zeldovich	2015-04-08
\|
*	Extraction: in support library, more and nicer big_int	letouzey	2010-06-15
\| \| \| \| \| \| \| \| \|	- 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	letouzey	2010-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	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	letouzey	2010-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: start of a support library	letouzey	2010-06-02
	- 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