coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| *	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
\| * \|	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
\| * \|	Fix description of command-line options in the manual.	Guillaume Melquiond	2016-01-06
* \| \|	TYPOGRAPHY: correction of one particular error in the Reference Manual	Matej Kosik	2015-12-18
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\| \|
\| * \|	Updating credits.	Hugo Herbelin	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
* \| \|	Simplifying documentation of "assert form as pat".	Hugo Herbelin	2015-12-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\| \|
\| * \|	Fix \label which was meants to be \ref in doc of CIC terms.	Maxime Dénès	2015-12-14
\| * \|	Remove a mention of Set Virtual Machine in doc.	Maxime Dénès	2015-12-14
\| * \|	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
\| * \|	Extraction: documentation of the new option Unset Extraction SafeImplicits	Pierre Letouzey	2015-12-12
\| * \|	Indexing and documenting some options.	Pierre-Marie Pédrot	2015-12-12
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\| \|
\| * \|	Remove Set Virtual Machine from doc, since the command itself has been removed.	Maxime Dénès	2015-12-11