coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix compilation and test-suite of nsatz	glondu	2010-07-12
*	Extraction: restrict autoinling to csts whose body is globally visible (fix #...	letouzey	2010-07-08
*	Extraction: more factorization of common match branches	letouzey	2010-07-08
*	Extraction: Unset Extraction AutoInline is now the default	letouzey	2010-07-08
*	nsatz in an integral domain with specialization to Z and R	pottier	2010-07-08
*	Extraction Library Foo creates Foo.ml, not foo.ml (correct version)	letouzey	2010-07-07
*	Extraction Library Foo creates Foo.ml, not foo.ml	letouzey	2010-07-07
*	Extraction: get advantage of nicer, algebraic, module types	letouzey	2010-07-07
*	Extraction: some more work on the (re)naming framework	letouzey	2010-07-07
*	Extraction: (yet another) rework of the renaming code	letouzey	2010-07-05
*	Extraction: better support of modules	letouzey	2010-07-02
*	Extraction: no more MPself hence no need for subst during pp	letouzey	2010-07-02
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau	2010-06-30
*	QArith: typo in name of hint db (fix #2346)	letouzey	2010-06-29
*	change the flag "internal" in declare/ind_tables from bool to	vsiles	2010-06-29
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Extraction: handling modules (not functors) in Haskell by name mangling	letouzey	2010-06-28
*	Extraction: remove a useless match	letouzey	2010-06-28
*	bug 2328 fixed: failure when polynomial not i ideal	pottier	2010-06-25
*	Extraction: nicer simple extraction of custom defs (fix #2204)	letouzey	2010-06-23
*	Names: remove obsolete mod_self_id	letouzey	2010-06-23
*	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey	2010-06-21
*	Extraction: fix the eta reduction function used in code optimisations	letouzey	2010-06-16
*	Extraction: in support library, more and nicer big_int	letouzey	2010-06-15
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Extraction Implicits: can accept argument names instead of just positions	letouzey	2010-06-10
*	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau	2010-06-09
*	Allowing to use an ordering different than Lt with measure	jforest	2010-06-09
*	Using vernac parsing for Function	jforest	2010-06-08
*	Extraction with implicits: perform the occur-check after optimisations	letouzey	2010-06-08
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08
*	Typo in ExtrOcamlString: list char instead of char list	letouzey	2010-06-08
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Extraction: attempt to provide nice extraction of chars and strings for Ocaml	letouzey	2010-06-04
*	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey	2010-06-04
*	plugins/xml: kill two warnings	letouzey	2010-06-03
*	Misc fixes related to new nsatz (and ocamlbuild)	letouzey	2010-06-03
*	nsatz ajoute	pottier	2010-06-03
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Fix typos	glondu	2010-06-02
*	Extraction: start of a support library	letouzey	2010-06-02
*	A little bit of cleanup, and some annotations.	fkirchne	2010-05-28
*	Modify the test for csdp and associated message.	fkirchne	2010-05-28
*	...	fkirchne	2010-05-28
*	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey	2010-05-21
*	Ocamlbuild: various fix	letouzey	2010-05-19
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19