coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
*	Updated CHANGES about subst. More on recursive equations in reference manual.	Hugo Herbelin	2016-06-29
*	Fixes in documentation.	Matthieu Sozeau	2016-06-29
*	Program: cleanup in cases, add options	Matthieu Sozeau	2016-06-29
*	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\
* \|	Documenting the "only printing" notation flag.	Pierre-Marie Pédrot	2016-06-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\ \
* \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| * \|	Reference Manual / Extraction: the original example command no longer works w...	Matej Kosik	2016-06-20
\| \| *	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\| \|/ \|/\|
* \|	par: like all: but in parallel	Enrico Tassi	2016-06-17
* \|	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
* \|	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
* \|	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\ \
* \| \|	typography	Matej Kosik	2016-06-15
\| * \|	Add documentation for goal selectors.	Cyprien Mangin	2016-06-14
* \| \|	-async-proofs-delegation-threshold default value set to 0.03	Enrico Tassi	2016-06-14
* \| \|	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \| \|/ / \|/\| \|
* \| \|	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\ \ \
* \| \| \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
* \| \| \|	typo	Matej Kosik	2016-06-07
* \| \| \|	typography	Matej Kosik	2016-06-07
\| \| * \|	Documentation	Enrico Tassi	2016-06-07
\| \|/ / \|/\| \|
\| * \|	Make Ltac Profiling an setting	Jason Gross	2016-06-05
\| * \|	Synchronize the profiler state with the document	Jason Gross	2016-06-05
\| * \|	-profileltac -> -profile-ltac, as per @herbelin	Jason Gross	2016-06-05
\| * \|	Add LtacProf documentation	Jason Gross	2016-06-05
\|/ /
* \|	Adding the Print Ltac Signature command.	Pierre-Marie Pédrot	2016-06-05
* \|	Fix build of documentation (broken for four months).	Guillaume Melquiond	2016-06-03
* \|	Fix a really small doc typo	Ricky Elrod	2016-05-15
* \|	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-05-02
\|\\|
\| *	Update tutorial (fix bug #4699).	Guillaume Melquiond	2016-04-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\\|
\| *	FIX: HTML version of Chapter 4 of the Reference Manual	Matej Kosik	2016-04-12
\| *	TYPOGRAPHY: adding missing \noindent macros	Matej Kosik	2016-04-12
* \|	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-05
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Document Hint Mode, cleanup Hint doc.	Matthieu Sozeau	2016-02-24
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
\| * \|	Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.	Maxime Dénès	2016-01-20
\| * \|	Documenting Set Bullet Behavior.	Hugo Herbelin	2016-01-20
\| * \|	Clarifying the documentation of tactics "cbv" and "lazy".	Hugo Herbelin	2016-01-20
\| * \|	Thanks Hugo, but let's remain factual.	Maxime Dénès	2016-01-15
* \| \|	Updating and improving the documentation of intros patterns.	Hugo Herbelin	2016-01-14
\| * \|	MMaps: remove it from final 8.5 release, since this new library isn't mature ...	Pierre Letouzey	2016-01-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\| \|
\| * \|	Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.	Hugo Herbelin	2016-01-12