coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin	2015-03-25
*	Another example about the consequence of a wrong computation of the	Hugo Herbelin	2015-03-25
*	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
*	Fixing wrong rel_context in checking positivity condition.	Hugo Herbelin	2015-03-24
*	Share more information between constructors and arity of an inductive	herbelin	2013-05-08
*	Moved isolated test params_ind.v to Inductive.v.	herbelin	2013-05-08
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	"Let in" in pattern hell, one more iteration	pboutill	2012-03-02
*	Partial fix for accepting bound variables with same name as implicit	herbelin	2011-05-26
*	fixed minor pbs with test cases	barras	2010-03-12
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin	2009-08-11
*	Test bug 983	herbelin	2006-01-20
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	Ajout exemple parametres implicites	herbelin	2003-10-08
*	Check local definitions in context of inductive types	herbelin	2003-09-06