coq - The formal proof system

Age	Commit message (Expand)	Author
2011-05-13	A new mechanism to handle errors.	aspiwack
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-10-31	An experimental support for open constrs in hints and in "using"	herbelin
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-28	Remove "init" label from Termops.it_mk* specialized functions	glondu
2010-06-30	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau
2010-06-14	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-03	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
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