coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#449: make specialize smarter (bug 5370).	Maxime Dénès	2017-06-01
\|\
\| *	Documenting the new behaviour of specialize.	Pierre Courtieu	2017-05-31
* \|	Documentation for eassert, eenough, epose proof, eset, eremember, epose.	Hugo Herbelin	2017-05-30
\|/
*	Documenting relaxing of constraints on injection.	Hugo Herbelin	2017-05-17
*	Improve documentation of assert / pose proof / specialize.	Théo Zimmermann	2017-05-04
*	Fixing #5420 as well as many related bugs due to miscounting let-ins.	Hugo Herbelin	2017-04-09
*	Fix broken documentation in presence of \zeroone{... \tt ...}.	Guillaume Melquiond	2016-12-06
*	Update documentation (bugs #5246 and #5251).	Guillaume Melquiond	2016-12-06
*	Merge remote-tracking branch 'github/pr/348' into v8.6	Maxime Dénès	2016-11-08
\|\
* \	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\|\ \
\| * \|	Document two new variants of refine	Matthieu Sozeau	2016-11-07
\| \| *	Minor fix in documentation	Matthieu Sozeau	2016-11-05
\| \|/ \|/\|
* \|	Merge remote-tracking branch 'github/pr/336' into v8.6	Maxime Dénès	2016-11-04
\|\ \
\| \| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
\| \| *	Documenting changes in typeclasses	Matthieu Sozeau	2016-10-29
\| \|/ \|/\|
\| *	Remove v62 from the refman.	Théo Zimmermann	2016-10-25
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-24
\|\ \ \| \|/ \|/\|
\| *	Documenting Hint Resolve -> and <- variants.	Théo Zimmermann	2016-10-19
\| *	Making the doc of auto hints more precise.	Théo Zimmermann	2016-10-19
\| *	Extending the doc with a general summary of auto variants.	Théo Zimmermann	2016-10-18
\| *	Document info_auto.	Théo Zimmermann	2016-10-18
\| *	Improve the documentation of eauto.	Théo Zimmermann	2016-10-18
* \|	fixing bug 4609: document an option governing the generation of equalities	Yves Bertot	2016-10-03
* \|	Merge branch 'v8.5' into v8.6	Maxime Dénès	2016-09-30
\|\\|
* \|	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	2016-09-28
\|\ \
\| \| *	Fixing #4887 (confusion between using and with in documentation of firstorder).	Hugo Herbelin	2016-09-27
* \| \|	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
* \| \|	Documenting "Set Structural Injection".	Hugo Herbelin	2016-08-21
* \| \|	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
\| * \|	Update the documentation for goal selectors.	Cyprien Mangin	2016-06-30
\|/ /
* \|	Updated CHANGES about subst. More on recursive equations in reference manual.	Hugo Herbelin	2016-06-29
* \|	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
* \|	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
* \|	Add documentation for goal selectors.	Cyprien Mangin	2016-06-14
* \|	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-03-05
\|\\|
\| *	Document Hint Mode, cleanup Hint doc.	Matthieu Sozeau	2016-02-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Clarifying the documentation of tactics "cbv" and "lazy".	Hugo Herbelin	2016-01-20
* \|	Updating and improving the documentation of intros patterns.	Hugo Herbelin	2016-01-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Documenting dtauto and dintuition.	Hugo Herbelin	2016-01-12
\| *	Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".	Hugo Herbelin	2016-01-12
\| *	Documenting option 'Set Bracketing Last Introduction Pattern'.	Hugo Herbelin	2016-01-12
\| *	restore documentation of admit	Enrico Tassi	2016-01-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond	2015-12-16
* \|	Simplifying documentation of "assert form as pat".	Hugo Herbelin	2015-12-15