aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2005-11-03*** empty log message ***mohring
2005-11-02Test reproductibilité du bug #1031herbelin
2005-09-09Declare Implicit Tacticherbelin
2005-09-09Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...herbelin
2005-09-08Test clear final dans intros patternherbelin
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
2005-03-21Ajout Unset Implicit Arguments manquantherbelin
2005-03-20Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...herbelin
2005-03-19Ajout test bug #935herbelin
2005-03-17Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
2005-03-16Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
2005-02-21*** empty log message ***herbelin
2005-02-17Test bug #922herbelin
2005-02-02test de la bonne position des vars de ltac entre les vars et les relsherbelin
2005-01-12The new tutorial on (co)inductive types by Pierre Casteran.sacerdot
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-10-27Ajout test dependent rewriteherbelin
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 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 17:04:37 +0000