coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Reference Manual / Extraction: the original example command no longer works ↵	Matej Kosik	2016-06-20
\| \| \| \|	with recent Coq
*	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.
*	Update tutorial (fix bug #4699).	Guillaume Melquiond	2016-04-28
\|
*	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
\|
*	Document Hint Mode, cleanup Hint doc.	Matthieu Sozeau	2016-02-24
\|
*	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
\|
*	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.
*	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
\|
*	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.
*	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
\|
*	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
\|
*	PROPOSITION: Added an explicit definition of the notation for enriching the ↵	Matej Kosik	2015-12-10
\| \| \| \|	global environment (we use throughout the document)
*	PROPOSITION: Added "if" and "then" words missing in the original sentence.	Matej Kosik	2015-12-10
\|
*	PROPOSITION: Example was simplified	Matej Kosik	2015-12-10
\|
*	DONE	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	TYPOGRAPHY	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: to do	Matej Kosik	2015-12-10
\|
*	GRAMMAR: added punctuation	Matej Kosik	2015-12-10
\|
*	CLEANUP PROPOSITION: rephrasing the original idea in a simpler way	Matej Kosik	2015-12-10
\|