coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Dont't forget to update the state or an obligation tactic assignment may	msozeau	2009-09-15
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
*	Hack to correctly get ill-formed rec body exceptions even	msozeau	2009-09-02
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	Support for definition hooks in subtac.	msozeau	2009-05-16
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20