aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementGravatar filliatr2002-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test de l'interprétation des fermetures de Match Context (2ème)Gravatar herbelin2002-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test de l'interprétation des fermetures de Match ContextGravatar herbelin2002-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests pour la tactique RegGravatar desmettr2002-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2777 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
* I added a comment on the tactic compute_POS.Gravatar bertot2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2767 85f007b7-540e-0410-9357-904b9bb8a0f7
* This example does not work in coq-7.3, but does in coq-7.2.Gravatar bertot2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exemple JCF conflit variable interne, variable de sectionGravatar herbelin2002-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des exemples sérieuxGravatar herbelin2002-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exemple Yves renommage différent d'une var de sectionGravatar herbelin2002-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructGravatar herbelin2002-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2755 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2750 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques bugs avec inject_natGravatar herbelin2002-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 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 herbelin2002-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test affichage O de nat dans une expression sur ZGravatar herbelin2002-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2440 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test de Pierre CrégutGravatar herbelin2002-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2420 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2418 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2002-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un test sur les anonymes dépendant dans des arguments implicitesGravatar herbelin2002-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test le filtrage dépendant vers l'avantGravatar herbelin2002-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2395 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un exemple de ChristineGravatar herbelin2001-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2365 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test sobriété de la réduction de IntuitionGravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test sobriété de la réduction de IntuitionGravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2350 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ GrammarGravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2338 85f007b7-540e-0410-9357-904b9bb8a0f7
* NatRing (2ème)Gravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2326 85f007b7-540e-0410-9357-904b9bb8a0f7
* NatRingGravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un peu plus d'inférence des ? traitée par le CasesGravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2323 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test des coercions dans les motifsGravatar herbelin2001-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 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
* Possibilité d'appeler check avec l'option -byteGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2235 85f007b7-540e-0410-9357-904b9bb8a0f7
* La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un bug dans le scriptGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2225 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
* Sur la cumulativité dans les tactiquesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux exemplesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2222 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2215 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2001-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2196 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques tests sur le let-inGravatar herbelin2001-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test syntaxe des constructions de l'état initialGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2132 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
* Mise en place d'un test de correction de la sortie de commandes CoqGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit par erreurGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test syntaxe des entiers relatifsGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test syntaxe des réelsGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2127 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 10:12:22 +0000