aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2002-07-05*** empty log message ***corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2839 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05Added a new uncompleteness bug found in Tauto.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2838 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-14*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2785 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Test de l'interprétation des fermetures de Match Context (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2782 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Test de l'interprétation des fermetures de Match Contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2780 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11Tests pour la tactique Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2777 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2768 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07I added a comment on the tactic compute_POS.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2767 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07This example does not work in coq-7.3, but does in coq-7.2.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2766 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout exemple JCF conflit variable interne, variable de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2764 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Des exemples sérieuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2762 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout exemple Yves renommage différent d'une var de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2759 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2755 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2750 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2726 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Quelques bugs avec inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2638 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2500 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25Test affichage O de nat dans une expression sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2440 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2438 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-21Ajout test de Pierre Crégutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2420 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2418 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2417 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-16Ajout d'un test sur les anonymes dépendant dans des arguments implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2400 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-15Test le filtrage dépendant vers l'avantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2366 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Ajout d'un exemple de Christineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2365 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Test sobriété de la réduction de Intuitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2351 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Test sobriété de la réduction de Intuitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2350 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJ Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2338 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19NatRing (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2326 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19NatRingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2325 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Un peu plus d'inférence des ? traitée par le Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2323 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2297 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11Test des coercions dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2238 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Possibilité d'appeler check avec l'option -byteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2235 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2230 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Un bug dans le scriptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2225 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Sur l'exahustivité du filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2224 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Sur la cumulativité dans les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2223 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Nouveaux exemplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2222 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2215 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2196 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Quelques tests sur le let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2173 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Test syntaxe des constructions de l'état initialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2132 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Test soumis par Randy Pollackherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2131 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Mise en place d'un test de correction de la sortie de commandes Coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2130 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Commit par erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2129 85f007b7-540e-0410-9357-904b9bb8a0f7