coq - The formal proof system

Age	Commit message (Expand)	Author
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-12	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin
2010-06-12	Added regression tests for bugs + miscellaneous improvements	herbelin
2010-06-12	Applying François' patch fixing grammar of uniform inheritance condition mes...	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
2010-06-07	fixing error message display.	vgross
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-06-03	Added command "Locate Ltac qid".	herbelin
2010-06-03	Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4	letouzey
2010-06-01	Cleanup: remove code specific for ocaml 3.06	letouzey
2010-06-01	restore handling of lexer errors	letouzey
2010-05-31	CoqIDE goes multiprocess	vgross
2010-05-31	More indirection.	vgross
2010-05-31	Introducing strong typing for IDE - toplevel IPC	vgross
2010-05-31	deporting Coq specific code from ide to toplevel.	vgross
2010-05-31	Modifying startup sequence	vgross
2010-05-29	New pass on inductive schemes	herbelin
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-05-19	Nicer representation of tokens, more independant of camlp*	letouzey
2010-05-19	static (and shared) camlp4use instead of per-file declaration	letouzey
2010-05-19	Remove compile-command pragmas for emacs	letouzey
2010-05-18	Applicative commutative cuts in Fixpoint guard condition	pboutill
2010-05-04	- Fixing bug #2308 about Lemma ... with	vsiles
2010-04-30	Fail: a way to check that a command is refused without blocking a script	letouzey
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Two forgotten $Id$ in last commit	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-27	Fix bug #2245, incorrect handling of Context in sections inside module	msozeau
2010-04-27	Added a new exception for already declared Schemes,	vsiles
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2010-04-22	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin
2010-04-20	missing space in error message	vsiles
2010-04-09	Granting wish #2249 (checking existing lemma name also when in a section).	herbelin
2010-03-30	Small improvements around coqdoc (including fix for bug #2288)	herbelin
2010-03-30	Improving error messages in the presence of utf-8 characters	herbelin
2010-03-29	Several bug-fixes and improvements of coqdoc	herbelin
2010-03-24	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin
2010-03-23	Added automatic expansion on the left of recursive notations	herbelin
2010-03-15	Fix splitting evars tactics and stop dropping evar constraints when	msozeau
2010-03-11	No delta-reduction in libtypes anymore	puech
2010-03-11	Filter out "_subproof" objects from search results	puech
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
2010-03-05	Minor fixes.	msozeau
2010-02-12	Delineating a API for Coq inside toplevel/vernac.ml	vgross
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-17	Variant !F M for functor application that does not honor the Inline declarations	letouzey