coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Use dashed lines for equivalence edges in dot output of universes	glondu	2011-01-11
*	Reverted r13715 "Add improved indenters that rely on the current proof state ...	gmelquio	2011-01-06
*	Remove Safe_marshal	glondu	2011-01-06
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Add improved indenters that rely on the current proof state to choose the ind...	gmelquio	2010-12-14
*	First release of Vector library.	pboutill	2010-12-10
*	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin	2010-12-03
*	Redirect stdout to stderr in -ideslave	glondu	2010-12-03
*	Fixing a bug introduced in r12304 (move of interpretation of	herbelin	2010-12-02
*	Do not throw an error for anonymous generalized binders as they will be	msozeau	2010-11-18
*	Remove redundant clause (and fix compatibility issue)	glondu	2010-11-16
*	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau	2010-11-15
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Add information of localisation when an error involving an "implicit	herbelin	2010-11-07
*	correcting a non catch error reported as an anomaly (Ploc.Exc)	jforest	2010-11-07
*	In Univ, unify order_request and constraint_type	glondu	2010-11-03
*	Output universe graph in DOT language if output file ends in .dot or .gv	glondu	2010-11-02
*	More generic Univ.dump_universes	glondu	2010-11-02
*	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