coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Qcabs : absolute value on normalized rational numbers Qc	Pierre Letouzey	2016-02-26
*	Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)	Pierre Letouzey	2016-02-26
*	Qcanon : implement some old suggestions by C. Auger	Pierre Letouzey	2016-02-26
*	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot	2016-02-23
*	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
*	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-29
\|\\|
\| *	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
* \|	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-21
\| *	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
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\\|
\| *	Put implicits back as in 8.4.	Matthieu Sozeau	2015-12-31
* \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \|	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
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Fix to previous commit (ClassicalFacts.v).	Hugo Herbelin	2015-12-05
* \|	Adding proofs on the relation between excluded-middle and minimization.	Hugo Herbelin	2015-12-05
* \|	Experimenting removing strong normalization of the mid-statement in tactic cut.	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Updating Compat85.v after bd1c97653 on bracketing last or-and	Hugo Herbelin	2015-11-10
* \|	Adding an amazing property of Prop.	Hugo Herbelin	2015-11-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Update compatibility file for some of bug #4392	Jason Gross	2015-11-03
* \|	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-10-09
\|\\|
\| *	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
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	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
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\\|
\| *	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