coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Extraction: multiple fixes related with the Not_found encountered by X. Leroy	letouzey	2010-09-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	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
*	Extraction: fix the eta reduction function used in code optimisations	letouzey	2010-06-16
*	Extraction with implicits: perform the occur-check after optimisations	letouzey	2010-06-08
*	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
*	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
*	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
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20