aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-10Cacher les .v8herbelin
2003-10-08Teste interaction ltac et modulesherbelin
2003-10-08Ajout exemple parametres implicitesherbelin
2003-10-08Test Conjectureherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-02Traduction des tests success et test en v8herbelin
2003-09-23Correction bug 328coq
2003-09-23test d'implicite incorrect depuis que eq porte sur Typebarras
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
2003-09-06Check local definitions in context of inductive typesherbelin
2003-09-03Projectionsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:24:20 +0000