coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Applicative commutative cuts in Fixpoint guard condition	pboutill	2010-05-18
*	better detection of nested recursion in Function	jforest	2010-05-07
*	Correction of a bug pointed by P. Casteran.	jforest	2010-05-07
*	Trying to find a problem pointed by P. Casteran	jforest	2010-05-07
*	Correction of bug 2290 (removing stupid message)	jforest	2010-05-04
*	Correction of bug 2290	jforest	2010-05-04
*	Extraction: fix type_expunge_from_sign broken in last commit	letouzey	2010-05-01
*	Extraction: an experimental command to get rid of some cst/constructor arguments	letouzey	2010-04-30
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Misc small fixes : warning, dep cycles, ocamlbuild...	letouzey	2010-04-26
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Extraction: cosmetics when using ocaml + Extract Inductive to symbols	letouzey	2010-04-16
*	Extraction: restore (temporarily?) a very limited form of linear letin reduction	letouzey	2010-04-16
*	Extraction: less eta in calls to global functions, better optimization phase	letouzey	2010-04-16
*	Extraction: improvement of optimizations (kill_dummy, optim_fix)	letouzey	2010-04-16
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Extraction: ad-hoc identifier type with annotations for reductions	letouzey	2010-04-16
*	Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e...	letouzey	2010-04-16
*	Look for csdp in $PATH at runtime, remove -csdpdir configure option	glondu	2010-04-11
*	Remove unused functions run_sdpa	glondu	2010-04-11