coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-04	Remove warning on SSR Search having moved.	Théo Zimmermann
2020-10-27	Rename operconstr -> term	Jim Fehrle
2020-10-26	adjust Search deprecation warning	Ralf Jung
2020-08-28	When reporting an implicit argument error on a rename argument, use the renam...	Hugo Herbelin
2020-05-18	[search] [ssr] Emit deprecated message when calling search from ssreflect	Emilio Jesus Gallego Arias
2020-05-15	Move SSR's Search to a new plugin and deprecate it.	Théo Zimmermann
2020-05-15	Search: new clauses for searching head, conclusion, kind...	Hugo Herbelin
2020-03-28	Remove SearchAbout command, deprecated in 8.5	Jim Fehrle
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-04	Add syntax for non maximally inserted implicit arguments	SimonBoulier
2019-12-22	Rename files with Class in their name to make their role clearer.	Pierre-Marie Pédrot
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-08-29	Make sure that all query commands return a notice (not an info) feedback	Maxime Dénès
2019-08-19	[api] Move handling of variable implicit data to impargs	Emilio Jesus Gallego Arias
2019-07-07	[error] Remove special error printing pre-processing	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-24	Stop using pstate in global print queries	Gaëtan Gilbert
2019-04-25	Add a typing colon in the output of the Search ssreflect vernacular	Erik Martin-Dorel
2019-04-12	Unify Set and Unset handling for options	Gaëtan Gilbert
2019-03-27	[plugins] [ssr] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2019-02-28	Implement a method for manual declaration of implicits.	Jasper Hugunin
2019-02-13	[ssr] move shorter Canonical to Coq proper	Enrico Tassi
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-02	coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax	Gaëtan Gilbert
2018-11-02	Command driven attributes.	Gaëtan Gilbert
2018-11-02	Move attributes out of vernacinterp to new attributes module	Gaëtan Gilbert
2018-10-19	Deprecating Global.type_of_global_in_context.	Hugo Herbelin
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot