coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Adding a proof of surjective pairing on vectors.	Hugo Herbelin	2015-08-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Adding a notation { x & P } for { x : _ & P }.	Hugo Herbelin	2015-08-02
\| *	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	The "on_last_hyp" tactic now behaves as it should.	Cyprien Mangin	2015-06-12
* \|	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
\| *	Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)	Guillaume Melquiond	2015-05-12
* \|	Tentatively setting cons and Some with 1st implicit argument maximal	Hugo Herbelin	2015-05-09
* \|	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
\| *	Fix instances of universe-polymorphic generalized rewriting to avoid	Matthieu Sozeau	2015-04-09
\| *	MMapAVL: some improved proofs + fix a forgotten Admitted	Pierre Letouzey	2015-04-02
\| *	MMapAVL: implementing MMapInterface via AVL trees	Pierre Letouzey	2015-04-02
\| *	ZArith/Int.v: some modernizations	Pierre Letouzey	2015-04-02
\| *	MMapPositive: some improvements	Pierre Letouzey	2015-04-02
\| *	Accomodating #4166 (providing "Require Import OmegaTactic" as a	Hugo Herbelin	2015-04-01
\| *	Fix various typos in documentation	Matěj Grabovský	2015-03-31
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| *	Add some missing Proof keywords.	Guillaume Melquiond	2015-03-06
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-03-06
\|\\|
\| *	MMapPositive: another implementation of MMaps	Pierre Letouzey	2015-03-06
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-03-05
\|\\|
\| *	MMaps again : adding MMapList, an implementation by ordered list	Pierre Letouzey	2015-03-05
\| *	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
* \|	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."	Maxime Dénès	2015-02-26
\| *	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond	2015-02-25
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-02-23
\|\\|
\| *	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-18
\|\\|
\| *	Fixing bug #4035 (support for dependent destruction within ltac code).	Hugo Herbelin	2015-02-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|
\| *	dependent destruction: Fix (part of) bug #3961, by fixing dependent *	Matthieu Sozeau	2015-02-14
* \|	Merge branch '8.5' into trunk	Matthieu Sozeau	2015-01-18
\|\\|
* \|	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-18
* \|	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau	2015-01-18
* \|	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau	2015-01-18
\| *	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau	2015-01-18
* \|	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