coq - The formal proof system

Age	Commit message (Expand)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-01-07	Fix test-suite fo non maximal implicit arguments	SimonBoulier
2019-10-01	Remove spurious uses of CoInductive in SSR prerequisite.	Pierre-Marie Pédrot
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-04-30	fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface	Georges Gonthier
2019-04-02	[ssr] under: rewrite takes an optional bool arg	Erik Martin-Dorel
2018-09-05	Fixing #8416 (Print Assumptions missing module information from compiled files).	Hugo Herbelin
2018-05-15	[ssr] import ssreflect test suite from math-comp	Enrico Tassi
2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin
2017-12-01	Cleanup API for registering universe binders.	Matthieu Sozeau
2017-11-25	Universe binders survive sections, modules and compilation.	Gaëtan Gilbert
2015-03-11	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi
2009-11-11	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-10-26	Local/Global revision 12418 continued	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2008-12-02	Add new directory for pre-compilation of files needed for further tests.	herbelin