coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès	2017-05-17
\|\
* \|	Adding an option "Printing Unfocused".	Pierre Courtieu	2017-05-04
\| *	Adding an even more compact mode for goal display.	Pierre Courtieu	2017-05-03
\|/
*	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
*	CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"	Matej Kosik	2016-08-26
*	CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"	Matej Kosik	2016-08-26
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/ /
* \|	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
* \|	Univs: local names handling.	Matthieu Sozeau	2015-10-28
* \|	Printing of @{} instances for polymorphic references in Print and About.	Matthieu Sozeau	2015-10-28
* \|	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
\|/
*	Generalisation of the "end command" argument of the goal printer.	Arnaud Spiwack	2015-03-31
*	Isolate a function for printing evar sets.	Hugo Herbelin	2015-01-24
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	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