coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-04	[notation] option to fine tune printing of literals	Enrico Tassi
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-03-19	Merge PR #11795: Print implicit arguments in types of references	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-12	Print implicit arguments in types of references	SimonBoulier
2020-02-23	parens --> parentheses	Abhishek Anand (optiplex7010@home)
2020-02-23	added the new option	Abhishek Anand (optiplex7010@home)
2019-12-06	Moving the diversity of constr printers to a label style.	Hugo Herbelin
2019-12-03	Printing: Interleaving search for notations and removal of coercions.	Hugo Herbelin
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2018-06-18	Remove reference name type.	Maxime Dénès
2018-05-08	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-11-21	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-10-25	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-08-01	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-14	Merge PR#765: Remove obsolete Show commands	Maxime Dénès
2017-06-14	[print] Allow Selective Printing of Notations	Emilio Jesus Gallego Arias
2017-06-12	Remove more dead code (follow-up of previous commit).	Théo Zimmermann
2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
2017-03-24	Renaming local_binder into local_binder_expr.	Hugo Herbelin
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-01-18	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
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-11-19	Printing function for [uconstr].	Arnaud Spiwack
2014-09-18	Fix debug printing with primitive projections.	Matthieu Sozeau
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-05-05	Now printing body of abbreviations (i.e. notation with a name) with	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-21	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot
2012-08-08	Updating headers.	herbelin
2012-07-12	Bug 2838: ExplApp in mutual inductive parameters	pboutill
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill