aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2004-06-02commentaireherbelin
2004-06-02Ajout tests affichage coercions vers Funclassherbelin
2004-06-02Ajout testsherbelin
2004-05-20Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...herbelin
2004-05-03Points-fixes avec let-inherbelin
2004-05-02Ajout test bug 711herbelin
2004-04-29Test bug 705herbelin
2004-04-28Ajout test If nouvelle syntaxeherbelin
2004-04-14Ajout exemple Brunoherbelin
2004-03-26*** empty log message ***barras
2004-03-24*** empty log message ***barras
2004-03-24bug de PP des fix (coqbugs #574)barras
2004-03-13Nouvel exemple; correction du contexte du précédentherbelin
2004-03-12Correctionsherbelin
2004-03-11Test l'interprétation des scopesherbelin
2004-03-11Ajout exemple Instherbelin
2004-03-11Ajout vieil exemple de coq-clubherbelin
2004-03-11Ajout d'un vieil exemple de N. Magaudherbelin
2004-03-11Ajout bug #540herbelin
2004-03-06the output the parser should produce nowbertot
2004-03-06changed the test for obj_magic.v to be less sensitive to changesbertot
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-28Exemple de Fredericherbelin
2004-02-27Ajout test synthese du predicat a partir du cast d'un filtrage avec dependancesherbelin
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
2004-02-06Test dependencies in constructorsherbelin
2004-02-06Ajout filtrage sur motifs dépendants dans des inductifs différentsherbelin
2004-02-04Vérification de la prise en compte des termes de type non inductifherbelin
2004-01-01[ -d ... ] au lieu de [ -f ... ] sur commit précédéntherbelin
2003-12-27Protection contre l'echec des tests parser pour la distribherbelin
2003-12-27Suppression en v8herbelin
2003-12-24BUGherbelin
2003-12-23Bug commit precedentherbelin
2003-12-23Renommages des hypotheses transformees car en raison des possibles dependance...herbelin
2003-12-17ajout test de non-regression Clear d'une def localebarras
2003-12-12Ajout exemple Yvesherbelin
2003-12-05Pour eviter d'avoir un gros type dans Setherbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-28Simplest Demo on modulescoq
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
2003-11-25CC: added injection theorycorbinea
2003-11-13Niveau V8herbelin
2003-11-13Fermeture de la section maintenant necessaireherbelin
2003-11-13Passage a un SStream predicatifherbelin
2003-11-09Test Generalizeherbelin
2003-10-27MAJherbelin
2003-10-14Test obsoleteherbelin
2003-10-13Cleaningherbelin
2003-10-11Logic_TypeSyntax disparuherbelin
2003-10-10*** empty log message ***herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:21:30 +0000