coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik	2017-06-01
*	Fix 3 unused-intro-pattern warnings in stdlib.	Théo Zimmermann	2017-03-14
*	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
*	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
*	Remove spaces from around list notations	Jason Gross	2016-09-26
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin	2016-04-27
*	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin	2016-04-27
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\
\| *	Fixing bug #4582: cannot override notation [ x ].	Pierre-Marie Pédrot	2016-02-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	List.nth_error directly produces Some/None instead of value/error	Pierre Letouzey	2015-05-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Prove [map_ext] using [map_ext_in].	Nickolai Zeldovich	2015-04-09
\| *	Add a [map_ext_in] lemma to List.v.	Nickolai Zeldovich	2015-04-09
\| *	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
* \|	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
* \|	Add two lemmas about firstn to the List standard library.	Sébastien Hinderer	2015-01-16
* \|	Lemmas related to the firstn function over lists.	Sébastien Hinderer	2015-01-16
* \|	ListSet: follow-up of Sebastien's last commit	Pierre Letouzey	2015-01-16
* \|	Work in progress on listset.	Sébastien Hinderer	2015-01-16
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...	Arnaud Spiwack	2014-12-28
*	Adds two lemmas about hderror to the List standard library.	Sébastien Hinderer	2014-12-18
*	Implement the nodup function on lists and prove associated results.	Sébastien Hinderer	2014-12-18
*	Lists: enhanced version of Seb's last commit on Exists/Forall	Pierre Letouzey	2014-12-18
*	Lists: a few results on Exists and Forall and a bit of code cleanup.	Sébastien Hinderer	2014-12-18
*	List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)	Pierre Letouzey	2014-12-11
*	First series of results on lists.	Sébastien Hinderer	2014-12-11
*	Clarifying the role of ListSet.v in the library, compared to other	Hugo Herbelin	2014-11-18
*	Improving printing of "[]" (nil) in spite of the risk of collision	Hugo Herbelin	2014-08-05
*	Testing a replacement of "cut" by "enough" on a couple of test files.	Hugo Herbelin	2014-08-05
*	More proofs independent of the names generated by induction/elim over	Hugo Herbelin	2014-08-05
*	Adding a generalized version of fold_Equal to FMapFacts.	Pierre Courtieu	2014-07-31
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06