aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
Commit message (Expand)AuthorAge
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
* Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
* Test suite file for a bug in int31 arithmetic fixed a while ago.Gravatar Maxime Dénès2016-03-25
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Fix test-suite fileGravatar Matthieu Sozeau2015-10-02
* | Extend test-suite for the positivity checker.Gravatar Arnaud Spiwack2015-06-24
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add test-suite file for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* Add another critical bug to the test-suite.Gravatar Maxime Dénès2014-04-09
* Test case containing a proof of false due to a DeBruijn off-by-one error in theGravatar Maxime Dénès2014-01-15
* Test case for the buggy commutative cut subterm rule.Gravatar Maxime Dénès2013-12-21
* test guard condition against feature incompatible with prop-extGravatar Bruno Barras2013-12-17
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Gravatar Matthieu Sozeau2013-12-17
* Fix name clash in "failure/inductive.v".Gravatar xclerc2013-09-20
* Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.Gravatar xclerc2013-09-20
* Merge "inductive?.v" tests into a single "inductive.v" test.Gravatar xclerc2013-09-20
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
* Uminus.v : prepare this test file for the use of FailGravatar letouzey2013-09-19
* universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesGravatar letouzey2013-09-19
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Fixing critical inductive polymorphism bug found by Bruno.Gravatar herbelin2011-10-05
* Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vGravatar herbelin2011-04-08
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added examples for checking that the guard condition excludes subtermsGravatar herbelin2010-05-20
* Fixed bug #2260 (check of resolution of all evars in the declarationGravatar herbelin2010-03-24
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* Fixed a bug introduced in revision 12265.Gravatar herbelin2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
* added tests for hyps reorderingGravatar barras2008-11-27
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* test module include w.r.t. universe constraintsGravatar barras2008-04-21
* Vérification que "rewrite in" se comporte comme "rewrite" et échoueGravatar herbelin2007-10-16
* Itération sur les sous-termes dans la vérification de la condition de gardeGravatar herbelin2007-09-06
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
* Tests de référence circulaire au sous-typage de module (pour mémoire)Gravatar herbelin2007-01-19
* Correction bug #1302Gravatar herbelin2007-01-17
* test condition de gardeGravatar barras2006-12-13
* Check that sort-polymorphic inductive types is not too laxGravatar herbelin2006-10-27
* Cette dérivation de paradoxe passait en V8.1betaGravatar herbelin2006-10-27