aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
Commit message (Collapse)AuthorAge
* fixed universes bug related to module inclusionGravatar barras2008-04-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10828 85f007b7-540e-0410-9357-904b9bb8a0f7
* test module include w.r.t. universe constraintsGravatar barras2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10827 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification que "rewrite in" se comporte comme "rewrite" et échoueGravatar herbelin2007-10-16
| | | | | | | | | sans bêta-normaliser face à un bêta-rédex dont l'argument ne correspond pas à ce qui est à réécrire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Itération sur les sous-termes dans la vérification de la condition de gardeGravatar herbelin2007-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests de référence circulaire au sous-typage de module (pour mémoire)Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1302Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
* test condition de gardeGravatar barras2006-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Check that sort-polymorphic inductive types is not too laxGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cette dérivation de paradoxe passait en V8.1betaGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation des tests suite à la modification de Rewrite .. in (r9201)Gravatar notin2006-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9239 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
| | | | | | | | | | | | InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stricte positivité en présence de types inductifs imbriqués avec ↵Gravatar herbelin2006-06-23
| | | | | | paramètres récursivement non uniformes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deux vérifications que le polymorphisme de sorte des inductifs ne ↵Gravatar herbelin2006-06-22
| | | | | | fonctionne pas incorrectement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8974 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction trou de typage des éliminations d'inductifs introduit dans ↵Gravatar herbelin2006-05-13
| | | | | | commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
* cf ltac4.vGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7686 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement params_indGravatar mohring2005-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7497 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite/output/Notations.outGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6308 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2004-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout test de non-regression Clear d'une def localeGravatar barras2003-12-17
| | | | | | | reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cacher les .v8Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4558 85f007b7-540e-0410-9357-904b9bb8a0f7
* test d'implicite incorrect depuis que eq porte sur TypeGravatar barras2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4455 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests ltacGravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test for redundant clausesGravatar herbelin2002-08-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputGravatar herbelin2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2768 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2638 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sur l'exahustivité du filtrageGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test soumis par Randy PollackGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test de dépendances de ClearBodyGravatar herbelin2001-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques signes extérieurs de la sémantique de Remark, question visibilitéGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests l'incohérence des universGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1931 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreurs de CasesGravatar mohring2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'erreurs sur le Case avec branche redondanteGravatar mohring2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1645 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de testsGravatar mohring2001-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1586 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'Apply dans TautoGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du test de TautoGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de testsGravatar mohring2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1087 85f007b7-540e-0410-9357-904b9bb8a0f7
* tests automatiquesGravatar herbelin2000-12-09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1082 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 14:22:51 +0000