aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
...
* I added a comment on the tactic compute_POS.Gravatar bertot2002-06-07
* This example does not work in coq-7.3, but does in coq-7.2.Gravatar bertot2002-06-07
* Ajout exemple JCF conflit variable interne, variable de sectionGravatar herbelin2002-06-06
* Des exemples sérieuxGravatar herbelin2002-06-06
* Ajout exemple Yves renommage différent d'une var de sectionGravatar herbelin2002-06-06
* Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructGravatar herbelin2002-06-05
* *** empty log message ***Gravatar herbelin2002-06-03
* *** empty log message ***Gravatar herbelin2002-05-29
* Quelques bugs avec inject_natGravatar herbelin2002-04-17
* *** empty log message ***Gravatar herbelin2002-04-12
* *** empty log message ***Gravatar herbelin2002-02-28
* Test affichage O de nat dans une expression sur ZGravatar herbelin2002-01-25
* *** empty log message ***Gravatar herbelin2002-01-25
* Ajout test de Pierre CrégutGravatar herbelin2002-01-21
* *** empty log message ***Gravatar herbelin2002-01-18
* *** empty log message ***Gravatar herbelin2002-01-18
* Ajout d'un test sur les anonymes dépendant dans des arguments implicitesGravatar herbelin2002-01-16
* Test le filtrage dépendant vers l'avantGravatar herbelin2002-01-15
* *** empty log message ***Gravatar herbelin2001-12-21
* Ajout d'un exemple de ChristineGravatar herbelin2001-12-21
* Test sobriété de la réduction de IntuitionGravatar herbelin2001-12-19
* Test sobriété de la réduction de IntuitionGravatar herbelin2001-12-19
* MAJ GrammarGravatar herbelin2001-12-19
* NatRing (2ème)Gravatar herbelin2001-12-19
* NatRingGravatar herbelin2001-12-19
* Un peu plus d'inférence des ? traitée par le CasesGravatar herbelin2001-12-19
* *** empty log message ***Gravatar herbelin2001-12-13
* Test des coercions dans les motifsGravatar herbelin2001-12-11
* *** empty log message ***Gravatar herbelin2001-11-21
* Possibilité d'appeler check avec l'option -byteGravatar herbelin2001-11-21
* La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...Gravatar herbelin2001-11-21
* Un bug dans le scriptGravatar herbelin2001-11-21
* Sur l'exahustivité du filtrageGravatar herbelin2001-11-21
* Sur la cumulativité dans les tactiquesGravatar herbelin2001-11-21
* Nouveaux exemplesGravatar herbelin2001-11-21
* *** empty log message ***Gravatar herbelin2001-11-20
* *** empty log message ***Gravatar herbelin2001-11-16
* Quelques tests sur le let-inGravatar herbelin2001-11-08
* Test syntaxe des constructions de l'état initialGravatar herbelin2001-10-17
* Test soumis par Randy PollackGravatar herbelin2001-10-17
* Mise en place d'un test de correction de la sortie de commandes CoqGravatar herbelin2001-10-17
* Commit par erreurGravatar herbelin2001-10-17
* Test syntaxe des entiers relatifsGravatar herbelin2001-10-17
* Test syntaxe des réelsGravatar herbelin2001-10-17
* *** empty log message ***Gravatar herbelin2001-10-15
* Test compatibilité V6 pour les filtrages avec let-inGravatar herbelin2001-10-15
* Test de dépendances de ClearBodyGravatar herbelin2001-10-05
* Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)Gravatar herbelin2001-10-03
* Tests de Cases avec définitions localesGravatar herbelin2001-10-03
* Tests noms longs de modulesGravatar herbelin2001-10-01