aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
Commit message (Expand)AuthorAge
* 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
* Adaptation des tests suite à la modification de Rewrite .. in (r9201)Gravatar notin2006-10-13
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Stricte positivité en présence de types inductifs imbriqués avec paramètr...Gravatar herbelin2006-06-23
* Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...Gravatar herbelin2006-06-22
* Correction trou de typage des éliminations d'inductifs introduit dans commit...Gravatar herbelin2006-05-13
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* cf ltac4.vGravatar herbelin2005-12-21
* deplacement params_indGravatar mohring2005-11-03
* test-suite/output/Notations.outGravatar herbelin2004-11-17
* *** empty log message ***Gravatar herbelin2004-10-17