coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| *	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 g...	Matej Kosik	2015-12-10
\| *	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
\| *	CLEANUP PROPOSITION: existing example was removed because it is not urgently ...	Matej Kosik	2015-12-10
\| *	ENH: existing example was changed so that it is now linked to the results sho...	Matej Kosik	2015-12-10
\| *	ENH: an existing example was further expanded.	Matej Kosik	2015-12-10
\| *	CLEANUP: Existing example was removed.	Matej Kosik	2015-12-10
\| *	ENH: existing example was expanded	Matej Kosik	2015-12-10
\| *	ENH: define the meaning of 'p'	Matej Kosik	2015-12-10
\| *	CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive definit...	Matej Kosik	2015-12-10
\| *	CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive de...	Matej Kosik	2015-12-10
\| *	COMMENT: question	Matej Kosik	2015-12-10
\| *	CLEANUP: removing a superfluous index	Matej Kosik	2015-12-10
\| *	COMMENT: question	Matej Kosik	2015-12-10
\| *	COMMENT: question	Matej Kosik	2015-12-10
\| *	GRAMMAR	Matej Kosik	2015-12-10
\| *	COMMENT: note	Matej Kosik	2015-12-10