aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Inductive.v
Commit message (Expand)AuthorAge
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Another example about the consequence of a wrong computation of theGravatar Hugo Herbelin2015-03-25
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Share more information between constructors and arity of an inductiveGravatar herbelin2013-05-08
* Moved isolated test params_ind.v to Inductive.v.Gravatar herbelin2013-05-08
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
* Partial fix for accepting bound variables with same name as implicitGravatar herbelin2011-05-26
* fixed minor pbs with test casesGravatar barras2010-03-12
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Test bug 983Gravatar herbelin2006-01-20
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Ajout exemple parametres implicitesGravatar herbelin2003-10-08
* Check local definitions in context of inductive typesGravatar herbelin2003-09-06