coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
*	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
*	Remove the unused printer_pr mechanism.	Jim Fehrle	2018-05-24
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| *	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
\|/
*	Print inductive cumulativity info in About.	Gaëtan Gilbert	2018-02-11
*	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
*	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\|/
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
* \	Merge PR #6103: Hack to restore printing of glob_constr in debugger.	Maxime Dénès	2017-11-13
\|\ \
\| * \|	Hack to restore printing of glob_constr in debugger.	Hugo Herbelin	2017-11-07
\| \| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|/ \|/\|
* \|	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\|/
*	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
*	Exporting the level-parametric printer of constr and its variants.	Hugo Herbelin	2017-11-02
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Add printing of cumulativity in inductive types	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	[emacs] [toplevel] Make emacs flag local to the toplevel.	Emilio Jesus Gallego Arias	2017-06-01
*	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