coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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