coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Improving error message when one instance-hole is not found.	Hugo Herbelin	2014-12-04
*	Moving mutual inductive printing from Printer to Printmod.	Pierre-Marie Pédrot	2014-11-20
*	Print [uconstr] in genargs.	Arnaud Spiwack	2014-11-19
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	Experimental printing of the signature of open evars in Check.	Hugo Herbelin	2014-10-17
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier	2014-09-01
*	Feedback: LoadedFile + Goals	Enrico Tassi	2014-07-11
*	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