coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-06-10	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey

2017-03-23	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès
	This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
2017-03-23	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès
	This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
2015-06-22	Add efficient extraction of [nat], [Z], and [string] to Haskell	Nickolai Zeldovich
	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
2015-04-08	add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.v	Nickolai Zeldovich

2010-06-15	Extraction: in support library, more and nicer big_int	letouzey
	- 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
2010-06-04	Extraction: attempt to provide nice extraction of chars and strings for Ocaml	letouzey
	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
2010-06-04	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02	Extraction: start of a support library	letouzey
	- 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