coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \|	Fixing bug #4684: Singleton list notation unusable in 8.5pl1.	Pierre-Marie Pédrot	2016-04-25
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\| \| \|
\| * \| \|	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
* \| \| \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \ \ \
* \ \ \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\ \ \ \ \ \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Fix handling of arity of definitional classes.	Matthieu Sozeau	2016-03-24
* \| \| \| \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
* \| \| \| \|	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
\| \| \| \| *	Update Coq84.v	Jason Gross	2016-01-12
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	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
\| \| \| *	Move compatibility notations to their proper files	Jason Gross	2015-12-29
\| \| \|/ \| \|/\|
* \| \|	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