coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-23	Merge PR #13804: [stdlib] [List] Add results about count_occ	coqbot-app[bot]
2021-01-29	add results on count_occ	Olivier Laurent
2021-01-08	Modify Sorting/Sorted.v to compile with -mangle-names	Jasper Hugunin
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-08-12	Additional statements about List.repeat	Olivier Laurent
2020-05-08	Declare more Permutation instances as Global	Olivier Laurent
2020-05-06	Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and m...	Hugo Herbelin
2020-05-03	consistency with Permutation	Olivier Laurent
2020-04-30	Symmetry in conclusions of List.map_eq_*	Olivier Laurent
2020-04-23	Merge PR #12120: Fixing #12119 : remove useless hypothesis in NoDup_Permutati...	Hugo Herbelin
2020-04-19	A library on cyclic permutations: CPermutation	Olivier Laurent
2020-04-19	remove useless hypothesis in NoDup_Permutation_bis	Olivier Laurent
2020-04-01	Add complementary results about Permutation	Olivier Laurent
2020-03-26	Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sort	Hugo Herbelin
2020-03-23	Fix levels of `<=?` and `<?` in the stdlib	Jason Gross
2020-03-23	Sorting: Swap the names of Sorted_sort and LocallySorted_sort	Lysxia
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-11-25	PermutEq: use “lia” rather than “omega”	Vincent Laporte
2019-11-25	PermutSetoid: use “lia” rather than “omega”	Vincent Laporte
2019-08-26	Make kernel parametric on the lowest universe and fix #9294	Matthieu Sozeau
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-25	Modifying theories to preferably use the "[= ]" syntax, and,	Hugo Herbelin
2019-05-23	Fixing typos - Part 3	JPR
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-04-13	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias
2018-03-07	[stdlib] Do not use “Require” inside sections	Vincent Laporte
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-01	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik
2016-06-18	Giving a more natural semantics to injection by default.	Hugo Herbelin
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-21	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-06-26	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond
2014-06-04	Make standard library independent of the names generated by	Hugo Herbelin
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-02-07	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey
2013-06-02	Making the behavior of "injection ... as ..." more natural:	herbelin
2012-08-08	Updating headers.	herbelin
2012-07-10	isolate instances about Permutation and PermutationA which may slow rewrite	letouzey
2012-07-09	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey