coq - The formal proof system

Age	Commit message (Expand)	Author
2017-11-24	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-21	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias
2017-11-13	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-07	Hack to restore printing of glob_constr in debugger.	Hugo Herbelin
2017-11-06	[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-04	Finish removing Show Goal uid	Gaëtan Gilbert
2017-11-02	Exporting the level-parametric printer of constr and its variants.	Hugo Herbelin
2017-10-25	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-16	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-01	[emacs] [toplevel] Make emacs flag local to the toplevel.	Emilio Jesus Gallego Arias
2017-05-17	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès
2017-05-04	Adding an option "Printing Unfocused".	Pierre Courtieu
2017-05-03	Adding an even more compact mode for goal display.	Pierre Courtieu
2017-02-14	Removing compatibility layers related to printing.	Pierre-Marie Pédrot
2017-02-14	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot
2016-08-26	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-06-16	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-11-02	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin
2015-10-28	Univs: local names handling.	Matthieu Sozeau
2015-10-28	Printing of @{} instances for polymorphic references in Print and About.	Matthieu Sozeau
2015-06-29	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi
2015-03-31	Generalisation of the "end command" argument of the goal printer.	Arnaud Spiwack
2015-01-24	Isolate a function for printing evar sets.	Hugo Herbelin
2015-01-17	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-12-04	Improving error message when one instance-hole is not found.	Hugo Herbelin
2014-11-20	Moving mutual inductive printing from Printer to Printmod.	Pierre-Marie Pédrot
2014-11-19	Print [uconstr] in genargs.	Arnaud Spiwack
2014-11-19	Printing function for [uconstr].	Arnaud Spiwack
2014-10-17	Experimental printing of the signature of open evars in Check.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-01	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier
2014-07-11	Feedback: LoadedFile + Goals	Enrico Tassi
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-11-02	Adds a shelve tactic.	aspiwack
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-05-14	Removing useless uses of Gmap.	ppedrot