coq - The formal proof system

Age	Commit message (Expand)	Author
2011-05-19	Extraction: avoid lots of late mind_of_kn	letouzey
2011-05-18	Extraction: avoid printing of Recursive Extraction in coqide's console	letouzey
2011-05-05	Extraction: allow extraction foo when foo is an alias notation	letouzey
2011-04-15	Extraction: nicer error when a toplevel module has no body (#2525)	letouzey
2011-04-13	Extraction: opaque terms are not traversed anymore by default	letouzey
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-07	Extraction: a warning when an opaque constant is enterred	letouzey
2011-03-07	A new command "Separate Extraction"	letouzey
2011-03-04	Extraction: improved indentation of extracted code (fix #2497)	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	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-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-05	Extraction: (yet another) rework of the renaming code	letouzey
2010-07-02	Extraction: better support of modules	letouzey
2010-07-02	Extraction: no more MPself hence no need for subst during pp	letouzey
2010-06-28	Extraction: remove a useless match	letouzey
2010-06-23	Extraction: nicer simple extraction of custom defs (fix #2204)	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-21	This big commit addresses two problems:	soubiran
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey