coq - The formal proof system

Age	Commit message (Expand)	Author
2020-01-19	Merge PR #11368: Turn trailing implicit warning into an error	Hugo Herbelin
2020-01-15	Discharge inductive types without rechecking them	Gaëtan Gilbert
2020-01-07	Fix test-suite fo non maximal implicit arguments	SimonBoulier
2018-10-31	No need to require List in test-suite/success/Inductive.v	Gaëtan Gilbert
2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin
2018-02-13	Fixing an anomaly in the presence of "let-in" in the type of a record.	Hugo Herbelin
2017-10-19	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann
2017-09-23	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin
2016-11-30	Fix UGraph.check_eq!	Matthieu Sozeau
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