aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2003-06-21Added a test for Functional Induction.courtieu
2003-05-22Test backtrackingherbelin
2003-05-21Nouveaux testsherbelin
2003-05-05Corrige Bug (PR#290)coq
2003-04-27Ce que Try récupèreherbelin
2003-04-15Débranchement des tests output qui sont faussés par le traducteurherbelin
2003-03-29indentationherbelin
2003-03-14*** empty log message ***barras
2003-03-04MAJherbelin
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
2003-02-27Adding tests for the "functional induction" facility.bertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 13:26:14 +0000