coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Typo in a comment of stdlib.	Hugo Herbelin	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
\| \|\ \
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\\| \| \|
* \| \| \|	Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...	Hugo Herbelin	2016-04-27
* \| \| \|	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin	2016-04-27
* \| \| \|	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin	2016-04-27
* \| \| \|	In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.	Hugo Herbelin	2016-04-27
* \| \| \|	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-04-27
* \| \| \|	Changing rule for "*" in Operator_Properties so that, iterated, it	Hugo Herbelin	2016-04-27
\| * \| \|	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