coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\|
*	CLEANUP PROPOSITION: existing example was removed because it is not urgently ↵	Matej Kosik	2015-12-10
\| \| \| \|	needed
*	ENH: existing example was changed so that it is now linked to the results ↵	Matej Kosik	2015-12-10
\| \| \| \|	shown in the previous example
*	ENH: an existing example was further expanded.	Matej Kosik	2015-12-10
\|
*	CLEANUP: Existing example was removed.	Matej Kosik	2015-12-10
\| \| \| \| \| \| \|	We have expanded the example above. For consistency reasons, it would make sense to do the same also for this example. However, due to the size of the terms, it is hard to typeset it nicely. I propose to remove it.
*	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 ↵	Matej Kosik	2015-12-10
\| \| \| \|	definition'? Doesn't make more sense to refer to it as 'inductive type'?
*	CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive ↵	Matej Kosik	2015-12-10
\| \| \| \|	definition.
*	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
\|
*	TYPOGRAPHY	Matej Kosik	2015-12-10
\|
*	CLEANUP: originally, we talked about "B" as an "arity"	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	ENH: a forward reference to a place where the concept of "allowed ↵	Matej Kosik	2015-12-10
\| \| \| \|	elimination sorts" is actually used
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	CLEANUP: unnecessary	Matej Kosik	2015-12-10
\|
*	GRAMMAR	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	ENH: improving precision	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	FIX: "u_p" was not defined	Matej Kosik	2015-12-10
\|
*	CLEANUP: removing duplicate paragraph	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: questions and to do	Matej Kosik	2015-12-10
\|