coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Noise for nothing	pboutill	2012-03-02
*	Avoid retrying uncessarily to prove independent remaining obligations in Prog...	msozeau	2012-02-15
*	Proof using ...	gareuselesinge	2011-12-12
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Fix compilation error	msozeau	2011-06-30
*	Keep obligation source information in Program	msozeau	2011-06-30
*	Call process_vernac_interp_error before calling Errors.print in	herbelin	2011-06-10
*	Fix bug #2415: warn when closing modules or sections and some obligations are...	msozeau	2011-06-07
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Add a flag to hide obligations in Program-generated terms under an	msozeau	2011-02-28
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Oops, don't use zeta by default.	msozeau	2010-03-15
*	Fix splitting evars tactics and stop dropping evar constraints when	msozeau	2010-03-15
*	Add a generic tactic option builder. Use it in firstorder to set the	msozeau	2010-03-05
*	Add [Next Obligation with tactic] support (wish #1953).	msozeau	2010-01-26
*	- Show Obligation Tactic	msozeau	2010-01-14
*	Support "Local Obligation Tactic" (now the default in sections).	msozeau	2010-01-11
*	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