aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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-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
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-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-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-11Logic_TypeSyntax disparuherbelin
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-09-23Correction bug 328coq
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-04-27Ce que Try récupèreherbelin
2003-03-29indentationherbelin
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
2003-01-28MAJ pour Regdesmettr
2003-01-22*** empty log message ***barras
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin