coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
* \|	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 ↵	Matthieu Sozeau	2016-04-04
\|\ \ \| \| \| \| \| \| \| \| \|	into JasonGross-trunk-function_scope
* \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it.
\| * \|	Clarifying the documentation of tactics "cbv" and "lazy".	Hugo Herbelin	2016-01-20
\| \| \| \| \| \| \| \| \| \| \| \|	Following a discussion on coq-club on Jan 13, 2016.
\| * \|	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
\| \| \| \| \| \| \| \| \| \| \| \|	In particular, documenting bracketing of last pattern on by default.
\| * \|	MMaps: remove it from final 8.5 release, since this new library isn't mature ↵	Pierre Letouzey	2016-01-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now.
* \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
* \| \|	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
\| \| \|
\| * \|	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| \| \| \| \| \| \| \| \| \| \| \|	Marking it as experimental.
\| * \|	Refman, ch. 4: A few fixes.	Hugo Herbelin	2015-12-10
\| \| \|
\| * \|	ENH: redundant examples were removed	Matej Kosik	2015-12-10
\| \| \|
\| * \|	FIX: wrong reference to a figure	Matej Kosik	2015-12-10
\| \| \|
\| * \|	CLEANUP: putting examples inside "figure" environment	Matej Kosik	2015-12-10
\| \| \|
\| * \|	ENH: The definition of the "_ ; _" operation on local context was added.	Matej Kosik	2015-12-10
\| \| \|
\| * \|	TYPOGRAPHY: adjustments	Matej Kosik	2015-12-10
\| \| \|
\| * \|	PROPOSITION: the side-condition was made more specific.	Matej Kosik	2015-12-10
\| \| \|
\| * \|	PROPOSITION: rephrasing of the explanation of the meaning of '[I:A\|B]'	Matej Kosik	2015-12-10
\| \| \|