coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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
\|
*	FIX: removing references to Γ which is not defined in a given context	Matej Kosik	2015-12-10
\|
*	TYPESETTING	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	GRAMMAR	Matej Kosik	2015-12-10
\|
*	CLEANUP PROPOSITION: superfluous parentheses were removed	Matej Kosik	2015-12-10
\|
*	CLEANUP PROPOSITION: s/local context of parameters/context of parameters	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: questions	Matej Kosik	2015-12-10
\|
*	COMMENT: to do	Matej Kosik	2015-12-10
\|
*	COMMENT: to do	Matej Kosik	2015-12-10
\|
*	FIX: removing a reference to \Gamma, because it is undefined	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	FIX: making sure that my previous edits do not break HTML generation	Matej Kosik	2015-12-10
\|
*	COMMENT: questions	Matej Kosik	2015-12-10
\|
*	ENH: examples for 'strict positivity' were expanded	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	CLEANUP: s/List_A/List~A/g	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	CLEANUP: the definition of "type of constructor" was rephrased in order to ↵	Matej Kosik	2015-12-10
\| \| \| \|	make it more clear
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: question	Matej Kosik	2015-12-10
\|
*	COMMENT: to do	Matej Kosik	2015-12-10
\|
*	FIX: commit 315f771	Matej Kosik	2015-12-10
\|
*	CLEANUP: superfluous examples were removed	Matej Kosik	2015-12-10
\|
*	ENH: new example: "even"	Matej Kosik	2015-12-10
\|
*	ALPHA-CONVERSION: s/Length/has_length/g	Matej Kosik	2015-12-10
\|