coq - The formal proof system

Age	Commit message (Expand)	Author
2014-04-25	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-01-04	Lemmas: export standard proof terminator	Enrico Tassi
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-08-08	State Transaction Machine	gareuselesinge
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-03-14	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-05-04	- Fixing bug #2308 about Lemma ... with	vsiles
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin