coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	More code sharing between tactic notation and genarg interpretation.	Pierre-Marie Pédrot	2015-12-13
\|
*	Removing dead unsafe code in Genarg.	Pierre-Marie Pédrot	2015-12-12
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\
\| *	Document removal of Set Virtual Machine and -vm in CHANGES.	Maxime Dénès	2015-12-11
\| \|
\| *	Remove Set Virtual Machine from doc, since the command itself has been removed.	Maxime Dénès	2015-12-11
\| \|
\| *	Add tactic native_cast_no_check, analog to vm_cast_no_check.	Maxime Dénès	2015-12-11
\| \|
\| *	Fixing a pat%constr bug. Thanks to Enrico for reporting.	Hugo Herbelin	2015-12-10
\| \|
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| \| \| \| \| \| \| \|	Marking it as experimental.
\| *	Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing	Hugo Herbelin	2015-12-10
\| \| \| \| \| \| \| \|	"open Unix" from lib/system.ml.
\| *	Silently ignore requests to _not_ clear something when that something cannot ↵	Guillaume Melquiond	2015-12-10
\| \| \| \| \| \| \| \| \| \| \| \|	be cleared. This should fix the contrib failures on tactics like "destruct (0)".
\| *	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
\| \|
\| *	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