aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* *** 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
* *** empty log message ***Gravatar herbelin2001-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test compatibilité V6 pour les filtrages avec let-inGravatar herbelin2001-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2120 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
* Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)Gravatar herbelin2001-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests de Cases avec définitions localesGravatar herbelin2001-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests noms longs de modulesGravatar herbelin2001-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2088 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un fichier test pour setoidesGravatar clrenard2001-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification de la syntaxe des optionsGravatar herbelin2001-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test inférence prédicat en présence d'universGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refine et let-inGravatar filliatr2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2012 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
* Ces fichiers décrivent des comportements peut-être souhaités mais ↵Gravatar herbelin2001-09-19
| | | | | | actuellement non implantés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comportements peut-être souhaités mais en tout cas non officiellement pris ↵Gravatar herbelin2001-09-19
| | | | | | en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe des HintsGravatar herbelin2001-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1960 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
* Bug inférence du prédicat en présence de K-rédexGravatar herbelin2001-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix d'un bug de TautoGravatar delahaye2001-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de deux anciens bugsGravatar delahaye2001-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli d'hypotheses pour faire fonctionner les exemplesGravatar herbelin2001-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli d'hypotheses pour faire fonctionner les exemplesGravatar herbelin2001-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1747 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
* test Fourier, DiscrRGravatar mayero2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise a la norme lexicaleGravatar mohring2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decomposition de CasesGravatar mohring2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1651 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:40:04 +0000