coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14
*	NPeano : improve compatibility for this deprecated file via compat notations	Pierre Letouzey	2016-05-04
*	Int.v: simplify Jason's commit 5b4e3ace	Pierre Letouzey	2016-05-04
*	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...	Pierre Letouzey	2016-05-04
\|\
* \|	Fixing bug #4684: Singleton list notation unusable in 8.5pl1.	Pierre-Marie Pédrot	2016-04-25
* \|	Added compatibility coercions from Specif.v which were present in Coq 8.4.	Hugo Herbelin	2016-04-08
* \|	Add -compat 8.4 econstructor tactics, and tests	Jason Gross	2016-04-05
* \|	Fix bug #4656	Jason Gross	2016-04-05
* \|	Update Coq84.v	Jason Gross	2016-04-04
* \|	Add compatibility Nonrecursive Elimination Schemes	Jason Gross	2016-04-04
* \|	Fix handling of arity of definitional classes.	Matthieu Sozeau	2016-03-24
* \|	Fixing bug #4582: cannot override notation [ x ].	Pierre-Marie Pédrot	2016-02-19
* \|	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
* \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	MMaps: remove it from final 8.5 release, since this new library isn't mature ...	Pierre Letouzey	2016-01-13
* \|	Put implicits back as in 8.4.	Matthieu Sozeau	2015-12-31
\| *	Move compatibility notations to their proper files	Jason Gross	2015-12-29
\|/
*	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
*	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
*	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
*	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
*	Fix some typos.	Guillaume Melquiond	2015-12-07
*	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
*	Update compatibility file for some of bug #4392	Jason Gross	2015-11-03
*	Fix some typos.	Guillaume Melquiond	2015-10-14
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Remove the "exists" overrides from Program. (Fix bug #4360)	Guillaume Melquiond	2015-10-07
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
*	Remove Print Universe directive.	Matthieu Sozeau	2015-10-02
*	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
*	Add compatibility files (feature 4319)	Jason Gross	2015-09-30
*	Emphasizing that eta for vectors is an instance of caseS, as pointed	Hugo Herbelin	2015-09-08
*	Minor modifications to WeakFanTheorem.	Hugo Herbelin	2015-09-08
*	Adding a proof of eta on Vector.t of non-zero size.	Hugo Herbelin	2015-09-08
*	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
*	The "on_last_hyp" tactic now behaves as it should.	Cyprien Mangin	2015-06-12
*	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
*	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
*	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