coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Some fine-tuning after removal of automatic imports of coercions in r13310	herbelin	2010-07-23
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Amelioration dans Function	jforest	2010-07-16
*	Fix goal display when backtracking	vgross	2010-07-05
*	Stronger checks on coqtop termination, warning when zombies.	vgross	2010-07-05
*	Correct wrong handling of evars in instance definitions that prevented	msozeau	2010-06-29
*	change the flag "internal" in declare/ind_tables from bool to	vsiles	2010-06-29
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	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-12
*	Automatic introduction of names given before ":" in Lemma's and	herbelin	2010-06-09
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	fixing error message display.	vgross	2010-06-07
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Added command "Locate Ltac qid".	herbelin	2010-06-03
*	Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4	letouzey	2010-06-03
*	Cleanup: remove code specific for ocaml 3.06	letouzey	2010-06-01
*	restore handling of lexer errors	letouzey	2010-06-01
*	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-31
*	New pass on inductive schemes	herbelin	2010-05-29
*	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-19
*	Applicative commutative cuts in Fixpoint guard condition	pboutill	2010-05-18
*	- Fixing bug #2308 about Lemma ... with	vsiles	2010-05-04
*	Fail: a way to check that a command is refused without blocking a script	letouzey	2010-04-30
*	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-29
*	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-27
*	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-22
*	missing space in error message	vsiles	2010-04-20
*	Granting wish #2249 (checking existing lemma name also when in a section).	herbelin	2010-04-09
*	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-30
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29