coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-26	[recordops] complete API rewrite; the module is now called [structures]	Enrico Tassi
2021-03-09	Replace cl_index with cl_typ in coercionops.ml	Kazuhiko Sakaguchi
2021-01-04	Remember universe instances of constants in notations	Jasper Hugunin
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-04	Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.	Hugo Herbelin
2020-10-08	Dropping the misleading int argument of Pp.h.	Hugo Herbelin
2020-08-28	About: Add a mention that arguments have been renamed, if ever it is the case.	Hugo Herbelin
2020-08-28	Where there are several lists of implicit arguments, don't pretend names matter.	Hugo Herbelin
2020-08-28	Do not write "rename" for arguments in About, since these arguments are valid...	Hugo Herbelin
2020-08-28	When printing the type in About, use the renamed arguments.	Hugo Herbelin
2020-08-28	In "About", print all arguments, even if it is trailing list of _.	Hugo Herbelin
2020-07-15	[search] Don't use ad-hoc Dumpglob table for Search	Emilio Jesus Gallego Arias
2020-06-30	[declaremods] Remove abstraction of imperative module operations	Emilio Jesus Gallego Arias
2020-06-25	Generate names for anonymous polymorphic universes	Gaëtan Gilbert
2020-05-14	Generalize the interpretation of syntactic notation as reference to their head.	Pierre-Marie Pédrot
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-20	Merge PR #11143: In Print/Check/Show, adopt the view that the attached type i...	Emilio Jesus Gallego Arias
2020-02-12	Merge PR #11546: Remove the Template Check option.	Gaëtan Gilbert
2020-02-09	Remove the Template Check option.	Pierre-Marie Pédrot
2020-02-04	Add syntax for non maximally inserted implicit arguments	SimonBoulier
2020-01-30	Merge PR #11307: Remove the hacks relying on hardwired libobject tags.	Maxime Dénès
2020-01-09	Fix build after merge of #11164	Gaëtan Gilbert
2019-12-28	Extend `Print Canonical Projections` with a search functionality	Kazuhiko Sakaguchi
2019-12-22	Rename files with Class in their name to make their role clearer.	Pierre-Marie Pédrot
2019-12-22	Remove the hacks relying on hardwired libobject tags.	Pierre-Marie Pédrot
2019-12-08	When printing term together with its type, use info that term is in context.	Hugo Herbelin
2019-12-04	Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.	Hugo Herbelin
2019-11-20	make VernacArguments closer to user syntax	Gaëtan Gilbert
2019-10-31	[prettyp] remove `mod_ops` and `indirect_accessor` parameters	Gaëtan Gilbert
2019-10-31	restore red behaviour printing	Gaëtan Gilbert
2019-10-31	Print argument info as an Arguments command in About	Gaëtan Gilbert
2019-10-31	Move prettyp (Print implementation) to vernac/	Gaëtan Gilbert