aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2006-06-06+ ameliorating the tactic "functional induction"jforest
2006-05-31Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)herbelin
2006-05-31Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseherbelin
2006-05-28Adaptation au passage de sig2 dans Typeherbelin
2006-05-28Adaptation au passage de vector dans Typeherbelin
2006-05-28Adaptation au passage de option dans Typeherbelin
2006-05-22encore un exemple ne marchant pas, ni avec omega ni avec romegaletouzey
2006-05-19tests de Romegaletouzey
2006-05-13Correction trou de typage des éliminations d'inductifs introduit dans commit...herbelin
2006-05-10Conformité nouveaux principes: Declare Module non utilisable pour définir u...herbelin
2006-05-10Centralisation de la détection lettre/symbole par le lexeur dans les plages ...herbelin
2006-05-05Vieux bug de fin 2004 gardé pour mémoireherbelin
2006-04-28Ajout bug #1102herbelin
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-04-24Timide tentative de clarification du statut de l'opérateur de filtrageherbelin
2006-04-15Tests notationsherbelin
2006-04-15Test synchronisation chargement objets non logiquesherbelin
2006-03-22- Correction bug calcul mind_consnrealargs, introduit à la révisionherbelin
2006-03-05Ajout test relatif au bug #984herbelin
2006-03-02Ajout test bug 1089herbelin
2006-03-02Correction du bug 808: il est maintenant interdit de déclarer une assomption...coq
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
2006-01-30Prise en compte coercions autour des sous-termes filtrés (si non dépendants)herbelin
2006-01-23Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...herbelin
2006-01-20Test bug 983herbelin
2006-01-15Test utf-8herbelin
2006-01-11Test conflictuel - ajouté pour mémoireherbelin
2006-01-11Test or-patternsherbelin
2006-01-11Ajout test notation récursiveherbelin
2006-01-05Test choix conflit afficheur de nombres selon la présence ou pas d'une coercionherbelin
2006-01-02Affichage de 'O' (lettre) comme '0' (chiffre)herbelin
2005-12-30Test bug #1025herbelin
2005-12-27Mini-test d'extractionherbelin
2005-12-26Achèvement suppression traducteur dans contrib/interfaceherbelin
2005-12-23Test printing of Tactic Notation which was broken until dec 2005herbelin
2005-12-22Abandon tests syntaxe v7 (correction)herbelin
2005-12-22Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2005-12-22option '-top dir' now works also in batch mode; it is even necessary to ensur...herbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2005-12-21Abandon tests syntaxe v7; ajouts tests modulesherbelin
2005-12-21MAJ syntaxe v7 avant activation en syntaxe v8herbelin
2005-12-21Activation du test de Refine en v7 pour mémoire avant passage à la v8herbelin
2005-12-21Anciennement déplacé dans 'output'herbelin
2005-12-21cf ltac4.vherbelin
2005-12-18L'option -no-vm laisse la place à une option -vmherbelin
2005-11-03*** empty log message ***mohring
2005-11-03deplacement params_indmohring
2005-11-02Test reproductibilité du bug #1031herbelin
2005-11-02Ajout tests interactifsherbelin
2005-11-01Interactive test of Backherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 22:31:18 +0000