aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
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-27Ajout test bug 860herbelin
2004-12-09Réactivation des tests output avec test aussi de la nouvelle syntaxeherbelin
2004-12-09Ajout d'une version nouvelle syntaxeherbelin
2004-12-09MAJ avec les particularités de l'afficheur v7 de la V8herbelin
2004-12-09Test d'affichage d'un Fix donné avec /nherbelin
2004-12-09Fichier non traductible (référence à des objets invisibles ce qui empêche...herbelin
2004-12-09Intégré à Implicit.vherbelin
2004-12-09Ajout suffixe 8 pour test en nouvelle syntaxeherbelin
2004-12-09Plus de statut spécial pour Remarkherbelin
2004-12-09Désactivation du test du printer arithmétique v7herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 19:12:58 +0000