coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Removing useless uses of Gmap.	ppedrot	2013-05-14
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Improving error message in explain_cannot_find_well_typed_abstraction:	herbelin	2013-04-17
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Print univ constraints generated by a constant or inductive (when flag is set)	barras	2012-11-21
*	Updating headers.	herbelin	2012-08-08
*	A friendlier printing of remaining goals when no goal is focused.	aspiwack	2012-07-11
*	Change how the number of open goals is printed.	aspiwack	2012-07-04
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29