coq - The formal proof system

Age	Commit message (Expand)	Author
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-17	Extraction: multiple fixes related with the Not_found encountered by X. Leroy	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-15	Extraction: fix a bit the extraction under modules	letouzey
2010-07-08	Extraction: Unset Extraction AutoInline is now the default	letouzey
2010-07-07	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: some more work on the (re)naming framework	letouzey
2010-07-05	Extraction: (yet another) rework of the renaming code	letouzey
2010-06-10	Extraction Implicits: can accept argument names instead of just positions	letouzey
2010-06-08	Extraction with implicits: perform the occur-check after optimisations	letouzey
2010-05-21	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey
2010-04-30	Extraction: an experimental command to get rid of some cst/constructor arguments	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-16	Extraction: ad-hoc identifier type with annotations for reductions	letouzey
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	Cleaning of Nametab continued + fixed a compilation bug in previous commit.	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey