coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Updated CHANGES about subst. More on recursive equations in reference manual.	Hugo Herbelin	2016-06-29
*	CHANGES: document fix for #4726 too.	Matthieu Sozeau	2016-06-29
*	CHANGES: document fix for 4527 and compatibility.	Matthieu Sozeau	2016-06-29
*	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\
* \|	Update CHANGES and COMPATIBILITY	Matthieu Sozeau	2016-06-27
* \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| *	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\|/
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Mentioning goal selectors in CHANGES	Enrico Tassi	2016-06-17
*	Fix wrong tabulation in CHANGES	Matthieu Sozeau	2016-06-16
*	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
*	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-06-16
*	Merge PR #195: Complete is_* family of term-examining tactics.	Pierre-Marie Pédrot	2016-06-16
\|\
* \|	--print-version produces machine readable version info	Enrico Tassi	2016-06-16
\| *	Update CHANGES	Jason Gross	2016-06-16
* \|	Merge remote-tracking branch 'origin/pr/166' into trunk	Enrico Tassi	2016-06-14
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \ \ \| \|_\|/ \|/\| \|
\| * \|	Reporting about a few bug fixes (to be continued).	Hugo Herbelin	2016-06-09
* \| \|	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
\| \|/ \|/\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	In Regular Subst Tactic mode, ensure that the order of hypotheses is	Hugo Herbelin	2016-05-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\\|
\| *	Mention problems with fix of #4582 in CHANGES.	Maxime Dénès	2016-04-22
\| *	Mention #4548 (fixed) in CHANGES.	Maxime Dénès	2016-04-22
\| *	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
\| *	Add changelog for 8.5pl1 after the fact.	Maxime Dénès	2016-04-17
* \|	Fix after merge, the revert of Bind Scope applies to trunk only.	Matthieu Sozeau	2016-04-04
* \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \| \|	All arguments defined through ARGUMENT EXTEND declare a tactic scope.	Pierre-Marie Pédrot	2016-03-04
* \| \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
* \| \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \| \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Reporting about the new tactical unshelve.	Hugo Herbelin	2016-01-12
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\| \|
\| * \|	Update version numbers and magic numbers for 8.5rc1 release.	Maxime Dénès	2015-12-16
\| * \|	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond	2015-12-16
\| * \|	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\| \|
\| * \|	Updating CHANGES with an incompatibility.	Hugo Herbelin	2015-12-14
\| * \|	Flag -compat 8.4 now loads Coq.Compat.Coq84.	Maxime Dénès	2015-12-14
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\| \|
\| * \|	Document removal of Set Virtual Machine and -vm in CHANGES.	Maxime Dénès	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
\|\\| \|
\| * \|	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
\| * \|	Fix CHANGES.	Hugo Herbelin	2015-12-05
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\| \|
\| * \|	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02