coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#279: A few lemmas about iff and about orders on positive and Z	Maxime Dénès	2017-03-06
\|\
* \	Merge PR#273: Tidy stdlib	Maxime Dénès	2017-03-03
\|\ \
\| \| *	Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.	Hugo Herbelin	2017-03-03
\| \| *	Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.	Hugo Herbelin	2017-03-03
\| \| *	Completing "few lemmas about Zneg" with lemmas also about Zpos.	Hugo Herbelin	2017-03-03
\| \| *	A couple of other useful properties about compare_cont.	Hugo Herbelin	2017-03-03
\| \| *	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
\| \|/ \|/\|
* \|	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
\| *	Proof clean-up.	Théo Zimmermann	2017-01-30
\|/
*	Fix a typo in Hurkens.v comment	Jason Gross	2016-12-19
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\
\| *	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
\| *	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\| \|\
\| \| *	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
\| * \|	Merge remote-tracking branch 'github/pr/336' into v8.6	Maxime Dénès	2016-11-04
\| \|\ \
\| * \| \|	Silence option deprecation warnings in the compat file	Jason Gross	2016-11-04
\| \| * \|	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
\| \|/ /
\| \| *	Add Unset Use Unif Heuristics in Compat/Coq85	Matthieu Sozeau	2016-10-22
\| \|/
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\|
\| *	Fix previous commit.	Pierre-Marie Pédrot	2016-10-17
\| *	Merge PR #300 into v8.6	Pierre-Marie Pédrot	2016-10-17
\| \|\
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\| \|\ \
\| * \| \|	Little addition to 6eede071 for consistency of style in OrdersFacts.v.	Hugo Herbelin	2016-10-12
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \| \|
\| * \| \|	Fixing unexpected "noise" introduced in commit 24d5448c.	Hugo Herbelin	2016-10-06
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \| \|
\| * \| \|	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
\| \| * \|	Remove if_then_else. Use tryif instead.	Théo Zimmermann	2016-10-03
\| * \| \|	More tests for tactic "subst".	Hugo Herbelin	2016-10-02
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \| \|
\| \| \| *	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
\| \| \|/ \| \|/\|
\| * \|	ZDivEucl: notations in different scope to avoid a warning	Pierre Letouzey	2016-09-28
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\| \|
\| * \|	Remove spaces from around list notations	Jason Gross	2016-09-26
\| * \|	Remove spaces from around vector notations	Jason Gross	2016-09-26
\| * \|	Unbreak Ltac [ \| .. \| ] notation in -compat 8.5	Jason Gross	2016-09-26
\| * \|	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \|
* \| \|	extensionality: Handle dependently-used hypotheses	Jason Gross	2016-09-19
* \| \|	Adding an "extensionality in H" tactic which applies functional	Hugo Herbelin	2016-09-19
\| * \|	Further "decide equality" tests on demand of Jason.	Hugo Herbelin	2016-09-17
\| * \|	Extending "contradiction" so that it recognizes statements such as "~x=x" or ...	Hugo Herbelin	2016-09-15
\|/ /
* \|	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
* \|	no-refold patch	Paul Steckler	2016-09-09
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\|\\|
\| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
* \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\|\ \