aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/check
Commit message (Expand)AuthorAge
* Use the Makefile in test-suite/checkGravatar glondu2010-04-10
* Fix typos in test-suite scriptGravatar glondu2010-04-10
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
* Remove interface pluginGravatar glondu2009-12-02
* Fixing xml theory file export (was not consistent with coqdoc fileGravatar herbelin2009-11-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Add new directory for pre-compilation of files needed for further tests.Gravatar herbelin2008-12-02
* Skip complexity tests on demandGravatar glondu2008-09-07
* Renaming parser -> coq-parserGravatar glondu2008-08-18
* Fix bashism in test-suite/checkGravatar glondu2008-07-28
* Intégration de micromega ("omicron" pour fourier et sa variante sur Z,Gravatar herbelin2008-05-19
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Correction d'un bug dans check + ajout de testsGravatar notin2007-09-21
* TypoGravatar notin2007-08-10
* Modification de la test suite pour intégrer des tests spécifiques auxGravatar notin2007-08-10
* Un chouia de portabilité en plus et pas de test si pas de bogomipsGravatar herbelin2007-03-19
* MAJ test complexité pour considérer le cas d'un temps avec un nombreGravatar herbelin2007-03-17
* Correction petits bugs du check de la test-suiteGravatar herbelin2006-12-28
* Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0Gravatar herbelin2006-11-13
* bug test complexitéGravatar herbelin2006-11-03
* suite commit 9222 : rétablissement des tests autre que complexitéGravatar herbelin2006-10-06
* Ajout d'un répertoire de test de la complexitéGravatar herbelin2006-10-06
* option '-top dir' now works also in batch mode; it is even necessary to ensur...Gravatar herbelin2005-12-22
* Abandon tests syntaxe v7; ajouts tests modulesGravatar herbelin2005-12-21
* L'option -no-vm laisse la place à une option -vmGravatar herbelin2005-12-18
* Ajout tests interactifsGravatar herbelin2005-11-02
* Suppression des fichiers temporairesGravatar herbelin2005-02-22
* Réactivation des tests output avec test aussi de la nouvelle syntaxeGravatar herbelin2004-12-09
* Suppression bruit perlGravatar herbelin2004-11-28
* bug de PP des fix (coqbugs #574)Gravatar barras2004-03-24
* changed the test for obj_magic.v to be less sensitive to changesGravatar bertot2004-03-06
* [ -d ... ] au lieu de [ -f ... ] sur commit précédéntGravatar herbelin2004-01-01
* Protection contre l'echec des tests parser pour la distribGravatar herbelin2003-12-27
* CleaningGravatar herbelin2003-10-13
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Traduction des tests success et test en v8Gravatar herbelin2003-10-02
* Débranchement des tests output qui sont faussés par le traducteurGravatar herbelin2003-04-15
* correcting the treatment of many tactics that use quant_hyp in file xlate.mlGravatar bertot2002-10-06
* Possibilité d'appeler check avec l'option -byteGravatar herbelin2001-11-21
* Mise en place d'un test de correction de la sortie de commandes CoqGravatar herbelin2001-10-17
* tests automatiquesGravatar herbelin2000-12-09