coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ZDivEucl: notations in different scope to avoid a warning	Pierre Letouzey	2016-09-28
*	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
*	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
\|\ \
* \ \	Merge remote-tracking branch 'github/bug4978' into v8.6	Matthieu Sozeau	2016-08-18
\|\ \ \
* \| \| \|	Fix an occurrence of deprecated eqn syntax in stdlib.	Maxime Dénès	2016-08-18
\| * \| \|	Fix #4978: priorities of Equivalence instances	Matthieu Sozeau	2016-08-17
\|/ / /
* \| \|	Replacing deprecated Implicit Arguments in prelude.	Maxime Dénès	2016-07-18
* \| \|	Remove the swap tactic from the prelude.	Maxime Dénès	2016-07-18
* \| \|	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
\| \| *	Typo.	Hugo Herbelin	2016-07-13
* \| \|	Typo in a comment of stdlib.	Hugo Herbelin	2016-07-08
\| * \|	Program: Move ProofIrrelevance to Subset.v	Matthieu Sozeau	2016-07-08
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	Merge remote-tracking branch 'github/pr/199' into v8.5	Maxime Dénès	2016-07-06
\| \|\
* \| \|	Fix #4793: Coq 8.6 should accept -compat 8.6	Maxime Dénès	2016-07-06
\| * \|	Move option_map notation up	Jason Gross	2016-07-05
\| * \|	Restore option_map in FMapFacts	Jason Gross	2016-07-05
\| \| *	Compat84: Don't mess with stdlib modules	Jason Gross	2016-07-05
* \| \|	Typeclasses: use once in by clause for typeclass eauto	Matthieu Sozeau	2016-06-28
* \| \|	Add Unset Shrink Abstract/Obligations in Coq85	Matthieu Sozeau	2016-06-27
* \| \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \| \|	Remove unneded hints in NZGcd	Matthieu Sozeau	2016-06-16
* \| \|	setoid_rewrite: fix the Params resolution tactic	Matthieu Sozeau	2016-06-16
* \| \|	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau	2016-06-16
* \| \|	In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.	Hugo Herbelin	2016-06-16
* \| \|	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-06-16
* \| \|	Changing rule for "*" in Operator_Properties so that, iterated, it	Hugo Herbelin	2016-06-16
\| \| *	Unbreak singleton list-like notation (-compat 8.4)	Jason Gross	2016-06-09
\| \|/
* \|	Officially discontinue the experimental coq build via ocamlbuild	Pierre Letouzey	2016-06-08
* \|	Relying instead on the Coq85 inclusion!	Hugo Herbelin	2016-06-06
* \|	Mode "Bracketing Last Introduction Pattern" is on for 8.4	Hugo Herbelin	2016-06-06
* \|	Mode "Regular Subst Tactic" is on in 8.6.	Hugo Herbelin	2016-06-06
* \|	Merge remote-tracking branch 'github/pr/118' into trunk	Maxime Dénès	2016-06-06
\|\ \
* \| \|	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\\| \|
\| * \|	NPeano : improve compatibility for this deprecated file via compat notations	Pierre Letouzey	2016-05-04
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	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
\| \|\ \