coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Goptions: repair Unset for int options	letouzey	2011-03-17
*	Finish branching functions handling module errors (cf. r13886)	letouzey	2011-03-16
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	A few more betaiota on environments and types of error messages. Seems to	herbelin	2011-03-05
*	Filter out admitted subgoals from search results	glondu	2011-02-25
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	Annotations at functor applications:	letouzey	2011-02-11
*	Remove obsolete TheoryList	glondu	2011-02-10
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	More comments and less doublons in some mli	pboutill	2011-02-10
*	Started to fix the declarative proof mode (C-zar).	aspiwack	2011-02-10
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	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