aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Test printing of Tactic Notation which was broken until dec 2005Gravatar herbelin2005-12-23
* Abandon tests syntaxe v7 (correction)Gravatar herbelin2005-12-22
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-22
* option '-top dir' now works also in batch mode; it is even necessary to ensur...Gravatar herbelin2005-12-22
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Abandon tests syntaxe v7; ajouts tests modulesGravatar herbelin2005-12-21
* MAJ syntaxe v7 avant activation en syntaxe v8Gravatar herbelin2005-12-21
* Activation du test de Refine en v7 pour mémoire avant passage à la v8Gravatar herbelin2005-12-21
* Anciennement déplacé dans 'output'Gravatar herbelin2005-12-21
* cf ltac4.vGravatar herbelin2005-12-21
* L'option -no-vm laisse la place à une option -vmGravatar herbelin2005-12-18
* *** empty log message ***Gravatar mohring2005-11-03
* deplacement params_indGravatar mohring2005-11-03
* Test reproductibilité du bug #1031Gravatar herbelin2005-11-02
* Ajout tests interactifsGravatar herbelin2005-11-02
* Interactive test of BackGravatar herbelin2005-11-01
* Declare Implicit TacticGravatar herbelin2005-09-09
* Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...Gravatar herbelin2005-09-09
* Test clear final dans intros patternGravatar herbelin2005-09-08
* Consequence of allowing the numerical argument of auto to be an ident for ltacGravatar herbelin2005-05-23
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* Ajout Unset Implicit Arguments manquantGravatar herbelin2005-03-21
* Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...Gravatar herbelin2005-03-20
* Ajout test bug #935Gravatar herbelin2005-03-19
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-17
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-16
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
* Suppression des fichiers temporairesGravatar herbelin2005-02-22
* *** empty log message ***Gravatar herbelin2005-02-21
* Test bug #922Gravatar herbelin2005-02-17
* test de la bonne position des vars de ltac entre les vars et les relsGravatar herbelin2005-02-02
* The new tutorial on (co)inductive types by Pierre Casteran.Gravatar sacerdot2005-01-12
* Ajout test bug 860Gravatar herbelin2004-12-27
* Réactivation des tests output avec test aussi de la nouvelle syntaxeGravatar herbelin2004-12-09
* Ajout d'une version nouvelle syntaxeGravatar herbelin2004-12-09
* MAJ avec les particularités de l'afficheur v7 de la V8Gravatar herbelin2004-12-09
* Test d'affichage d'un Fix donné avec /nGravatar herbelin2004-12-09
* Fichier non traductible (référence à des objets invisibles ce qui empêche...Gravatar herbelin2004-12-09
* Intégré à Implicit.vGravatar herbelin2004-12-09
* Ajout suffixe 8 pour test en nouvelle syntaxeGravatar herbelin2004-12-09
* Plus de statut spécial pour RemarkGravatar herbelin2004-12-09
* Désactivation du test du printer arithmétique v7Gravatar herbelin2004-12-09
* Ajout bug do_restrict_hypGravatar herbelin2004-12-08
* Erreur commit précédentGravatar herbelin2004-12-06
* Ajout bug #888Gravatar herbelin2004-12-06
* Ajout bug #889Gravatar herbelin2004-12-06
* Failed in 8.0pl1Gravatar herbelin2004-12-04
* Was failing in 8.0pl1Gravatar herbelin2004-12-03
* Suppression bruit perlGravatar herbelin2004-11-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 12:00:10 +0000