aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2004-12-08Ajout bug do_restrict_hypherbelin
2004-12-06Erreur commit précédentherbelin
2004-12-06Ajout bug #888herbelin
2004-12-06Ajout bug #889herbelin
2004-12-04Failed in 8.0pl1herbelin
2004-12-03Was failing in 8.0pl1herbelin
2004-11-28Suppression bruit perlherbelin
2004-11-28Re-commit version nouvelle syntaxeherbelin
2004-11-28Passage à la v8 pour test parserherbelin
2004-11-17Test lieurs dans Notationherbelin
2004-11-17test-suite/output/Notations.outherbelin
2004-10-27Ajout test dependent rewriteherbelin
2004-10-17*** empty log message ***herbelin
2004-10-14reflexivity, symmetry, symmetry ... in e transitivity now fall-backsacerdot
2004-10-07New commandssacerdot
2004-10-04Added "as ..." parameter to Add Morphism.sacerdot
2004-10-01Added "as ..." parameters to "Add Setoid"sacerdot
2004-09-30New tacticsacerdot
2004-09-30New tactic [setoid_]rewrite ... in ... [generate side conditions ...].sacerdot
2004-09-29Test updated.sacerdot
2004-09-25Ajoutsherbelin
2004-09-24Ajout bug #255herbelin
2004-09-03* New test (for setoid_replace in the general case)sacerdot
2004-09-03* setoid_test.v removed and added again in new syntaxsacerdot
2004-08-23The previous test file was truncated. New commit to fix the previoussacerdot
2004-07-23Several tests for the bug-fixed and improved new version ofsacerdot
2004-07-16Nouvelle en-têteherbelin
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