coq - The formal proof system

Age	Commit message (Expand)	Author
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