coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-05	Add a generic tactic option builder. Use it in firstorder to set the	msozeau
2010-01-26	Add [Next Obligation with tactic] support (wish #1953).	msozeau
2010-01-14	- Show Obligation Tactic	msozeau
2010-01-11	Support "Local Obligation Tactic" (now the default in sections).	msozeau
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-15	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-02	Hack to correctly get ill-formed rec body exceptions even	msozeau
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-05-16	Support for definition hooks in subtac.	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey