coq - The formal proof system

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