coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	Restored checking that _all_ arguments of the command line are meaningful	herbelin	2010-11-01
*	Add tolerance for existential variables in Check.	herbelin	2010-10-31
*	Minor code improvements around libobject	herbelin	2010-10-31
*	Minor factorization of the part of the code used for Unnamed_thm saving.	herbelin	2010-10-31
*	Compatibility camlp4/camlp5	herbelin	2010-10-26
*	Fail, when successful, prints something only in verbose mode	glondu	2010-10-26
*	Fixing bug #2412, continued (preprocessing of Ltac Debug errors	herbelin	2010-10-23
*	Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).	herbelin	2010-10-23
*	About "unsupported" unicode characters in notations.	herbelin	2010-10-17
*	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin	2010-10-11
*	Fix bug# 2392	msozeau	2010-10-07
*	Remove Explain* vernacs	glondu	2010-10-06
*	Remove VernacGo	glondu	2010-10-06
*	Two [Evd.fold] turned into [Evd.fold_undefined].	aspiwack	2010-10-04
*	Avoid raising an anomaly when an error encapsulated with a dummy	herbelin	2010-10-03
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Making display of various informations about constants more modular:	herbelin	2010-10-03
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Fixed a bug in printing fix/cofix error messages when several	herbelin	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too	herbelin	2010-09-18
*	Fixing bugs #2347 (part 2) and #2388: error message printing was done	herbelin	2010-09-18
*	CoqIDE argv parsing delegated to coqtop	vgross	2010-09-14
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	* removed declare_constant and declare_internal_constant	vsiles	2010-09-02
*	v13392 port from v8.3 to trunk : correct message when defining inductive schemes	vsiles	2010-09-02
*	* By default, load proof terms.	regisgia	2010-08-31
*	* scripts/Coqc toplevel/Usage:	regisgia	2010-08-27
*	* toplevel/Coqtop: Reactivate -dont-load-proofs option.	regisgia	2010-08-27
*	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia	2010-08-27
*	Fix an error message ot having the ERror: prefix.	courtieu	2010-08-26
*	Rather quick hack to make basic unicode notations available by	herbelin	2010-07-29
*	Fix computation of fix annotation index: only consider assumptions and	msozeau	2010-07-27
*	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