aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
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-23Consequence of allowing the numerical argument of auto to be an ident for ltacherbelin
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-22Suppression des fichiers temporairesherbelin
2005-02-21*** empty log message ***herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 07:26:42 +0000