coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-10-22	FSets: do not use “omega”	Vincent Laporte
2019-10-04	[Stdlib] OrderedType: do not pollute the “core” hint database	Vincent Laporte
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-03-30	Error when [foo.(bar)] is used with nonprojection [bar]	Gaëtan Gilbert
2018-12-19	Put #[universes(template)] on all auto template spots in stdlib	Gaëtan Gilbert
2018-11-14	Deprecate hint declaration/removal with no specified database	Maxime Dénès
2018-09-10	Deprecate romega in favor of lia.	Vincent Laporte
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-06-14	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey
2014-09-27	Keyed unification option, compiling the whole standard library	Matthieu Sozeau
2014-06-26	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-07-05	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
2010-06-08	Made option "Automatic Introduction" active by default before too many	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-28	ZArith/Int: no need to load romega here (but rather in FullAVL)	letouzey
2008-04-03	New file FMapFullAVL containing the balancing proofs about FMapAVL:	letouzey